From 08a7997a97658ea9b4211cd44ef1e0103bbc6996 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Jan 2015 14:07:20 -0800
Subject: [PATCH] refactor(library/data/string): put is_inhabited theorems on
 the toplevel

---
 library/data/string.lean | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

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