--- 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"