--- a/src/HOL/TLA/Init.thy Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Init.thy Sun Mar 20 23:07:06 2011 +0100
@@ -14,8 +14,7 @@
typedecl behavior
arities behavior :: world
-types
- temporal = "behavior form"
+type_synonym temporal = "behavior form"
consts