types -> type_synonym

--- 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} *}
 

--- a/src/HOL/HOLCF/Tr.thy	Sun Dec 19 18:10:54 2010 -0800
+++ b/src/HOL/HOLCF/Tr.thy	Sun Dec 19 18:11:20 2010 -0800
@@ -10,7 +10,7 @@
 
 subsection {* Type definition and constructors *}
 
-types
+type_synonym
   tr = "bool lift"
 
 translations

--- a/src/HOL/HOLCF/Universal.thy	Sun Dec 19 18:10:54 2010 -0800
+++ b/src/HOL/HOLCF/Universal.thy	Sun Dec 19 18:11:20 2010 -0800
@@ -12,7 +12,7 @@
 
 subsubsection {* Basis datatype *}
 
-types ubasis = nat
+type_synonym ubasis = nat
 
 definition
   node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis"