
diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_2.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -8,9 +8,8 @@
   In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While.
 *}
 
-types
-  var = unit
-  state = bool
+type_synonym var = unit
+type_synonym state = bool
 
 datatype com =
   Skip |




