src/HOL/Predicate_Compile_Examples/Hotel_Example.thy

--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -6,7 +6,7 @@
 datatype key = Key0 | Key1 | Key2 | Key3
 datatype room = Room0
 
-types card = "key * key"
+type_synonym card = "key * key"
 
 datatype event =
    Check_in guest room card | Enter guest room card | Exit guest room