diff --git a/library/debugger/util.lean b/library/debugger/util.lean
index 3d0d3d0047..6b5f0c5642 100644
--- a/library/debugger/util.lean
+++ b/library/debugger/util.lean
@@ -19,12 +19,12 @@ def split (s : string) : list string :=
 (split_core s [])^.reverse
 
 def to_qualified_name_core : string → string → name
-| []      r := if r = [] then name.anonymous else mk_simple_name r^.reverse
+| []      r := if r = "" then name.anonymous else mk_simple_name r^.reverse
 | (c::cs) r :=
   if is_space c then to_qualified_name_core cs r
   else if c = #"." then
-       if r = [] then to_qualified_name_core cs []
-       else           name.mk_string r^.reverse (to_qualified_name_core cs [])
+       if r = ""   then to_qualified_name_core cs []
+       else             name.mk_string r^.reverse (to_qualified_name_core cs [])
   else to_qualified_name_core cs (c::r)
 
 def to_qualified_name (s : string) : name :=
diff --git a/library/init/instances.lean b/library/init/instances.lean
index bad511b45a..f5226cf551 100644
--- a/library/init/instances.lean
+++ b/library/init/instances.lean
@@ -14,6 +14,9 @@ by mk_dec_eq_instance
 instance {α : Type u} [decidable_eq α] : decidable_eq (list α) :=
 by mk_dec_eq_instance
 
+instance : decidable_eq string :=
+list.decidable_eq
+
 instance : decidable_eq occurrences :=
 by mk_dec_eq_instance
 
diff --git a/library/init/string.lean b/library/init/string.lean
index ad205a5614..037ea6e26a 100644
--- a/library/init/string.lean
+++ b/library/init/string.lean
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 prelude
 import init.char init.list
 
-@[reducible] def string := list char
+def string := list char
 
 namespace string
 @[pattern] def empty : string := list.nil