src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Thu Sep 27 22:22:08 2001 +0200
+++ b/src/HOL/Product_Type.thy	Thu Sep 27 22:22:58 2001 +0200
@@ -96,21 +96,15 @@
 
 (** unit **)
 
-global
-
 typedef unit = "{True}"
 proof
   show "True : ?unit"
     by blast
 qed
 
-consts
-  "()"          :: unit                           ("'(')")
-
-local
-
-defs
-  Unity_def:    "() == Abs_unit True"
+constdefs
+  Unity :: unit    ("'(')")
+  "() == Abs_unit True"