--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 07 10:05:19 2010 +0200
@@ -79,10 +79,10 @@
declare Let_def[code_pred_inline]
lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
-by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
+by (auto simp add: insert_iff[unfolded mem_def] ext_iff intro!: eq_reflection)
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)
+by (auto simp add: Diff_iff[unfolded mem_def] ext_iff intro!: eq_reflection)
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,