src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 42463 f270e3e18be5
parent 42208 02513eb26eb7
child 44890 22f665a2e91c
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -770,9 +770,8 @@
 
 subsection {* IMP *}
 
-types
-  var = nat
-  state = "int list"
+type_synonym var = nat
+type_synonym state = "int list"
 
 datatype com =
   Skip |