--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,13 +2,13 @@
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
begin
-datatype_new guest = Guest0 | Guest1
-datatype_new key = Key0 | Key1 | Key2 | Key3
-datatype_new room = Room0
+datatype guest = Guest0 | Guest1
+datatype key = Key0 | Key1 | Key2 | Key3
+datatype room = Room0
type_synonym card = "key * key"
-datatype_new event =
+datatype event =
Check_in guest room card
| Enter guest room card
| Exit guest room