src/HOL/HOLCF/One.thy

--- a/src/HOL/HOLCF/One.thy	Sun Dec 19 18:10:54 2010 -0800
+++ b/src/HOL/HOLCF/One.thy	Sun Dec 19 18:11:20 2010 -0800
@@ -8,14 +8,14 @@
 imports Lift
 begin
 
-types one = "unit lift"
-translations
-  (type) "one" <= (type) "unit lift" 
+type_synonym
+  one = "unit lift"
 
-definition
-  ONE :: "one"
-where
-  "ONE == Def ()"
+translations
+  (type) "one" <= (type) "unit lift"
+
+definition ONE :: "one"
+  where "ONE == Def ()"
 
 text {* Exhaustion and Elimination for type @{typ one} *}