diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -2,13 +2,13 @@
 imports Main
 begin
 
-datatype guest = Guest0 | Guest1
-datatype key = Key0 | Key1 | Key2 | Key3
-datatype room = Room0
+datatype_new guest = Guest0 | Guest1
+datatype_new key = Key0 | Key1 | Key2 | Key3
+datatype_new room = Room0
 
 type_synonym card = "key * key"
 
-datatype event =
+datatype_new event =
    Check_in guest room card | Enter guest room card | Exit guest room
 
 definition initk :: "room \<Rightarrow> key"