diff --git a/library/data/string.lean b/library/data/string.lean
index 1e0a738e6..3a53ad6bc 100644
--- a/library/data/string.lean
+++ b/library/data/string.lean
@@ -5,16 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.string
 Author: Leonardo de Moura
 -/
-
 import data.bool
-open bool inhabited
+open bool
 
-namespace char
-  protected definition is_inhabited [instance] : inhabited char :=
-  inhabited.mk (mk ff ff ff ff ff ff ff ff)
-end char
+protected definition char.is_inhabited [instance] : inhabited char :=
+inhabited.mk (char.mk ff ff ff ff ff ff ff ff)
 
-namespace string
-  protected definition is_inhabited [instance] : inhabited string :=
-  inhabited.mk empty
-end string
+protected definition string.is_inhabited [instance] : inhabited string :=
+inhabited.mk string.empty