typedef (open) unit

--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 13:37:17 2010 -0800
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Nov 16 16:36:57 2010 -0800
@@ -89,7 +89,7 @@
 
 lemma "Rep_unit () = True"
 nitpick [expect = none]
-by (insert Rep_unit) (simp add: unit_def)
+by (insert Rep_unit) simp
 
 lemma "Rep_unit () = False"
 nitpick [expect = genuine]

--- a/src/HOL/Product_Type.thy	Tue Nov 16 13:37:17 2010 -0800
+++ b/src/HOL/Product_Type.thy	Tue Nov 16 16:36:57 2010 -0800
@@ -37,7 +37,7 @@
 
 subsection {* The @{text unit} type *}
 
-typedef unit = "{True}"
+typedef (open) unit = "{True}"
 proof
   show "True : ?unit" ..
 qed
@@ -48,7 +48,7 @@
   "() = Abs_unit True"
 
 lemma unit_eq [no_atp]: "u = ()"
-  by (induct u) (simp add: unit_def Unity_def)
+  by (induct u) (simp add: Unity_def)
 
 text {*
   Simplification procedure for @{thm [source] unit_eq}.  Cannot use