src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38950 62578950e748
parent 38949 1afa9e89c885
child 38953 0c38eb5fc4ca
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:53 2010 +0200
@@ -84,12 +84,12 @@
 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
 by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
 
-ML {* Code_Prolog.options :=
+setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
   limited_types = [],
   limited_predicates = [],
   replacing = [],
-  prolog_system = Code_Prolog.SWI_PROLOG} *}
+  prolog_system = Code_Prolog.SWI_PROLOG}) *}
 
 values 40 "{s. hotel s}"