--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Wed Aug 22 22:55:41 2012 +0200
@@ -1,8 +1,9 @@
theory Hotel_Example_Small_Generator
imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
-uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
begin
+ML_file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
+
declare Let_def[code_pred_inline]
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"