--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Mar 12 21:41:11 2012 +0100
@@ -41,7 +41,7 @@
lemma Diff[code_pred_inline]:
"(A - B) = (%x. A x \<and> \<not> B x)"
- by (simp add: fun_eq_iff minus_apply)
+ by (simp add: fun_eq_iff)
lemma subset_eq[code_pred_inline]:
"(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
@@ -232,4 +232,4 @@
lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
unfolding less_nat[symmetric] by auto
-end
\ No newline at end of file
+end