diff -r 3c54878ed67b -r 732ea1f08e3f src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 30 10:08:00 2012 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Apr 30 12:14:51 2012 +0200
@@ -29,15 +29,7 @@
 declare Ball_def[code_pred_inline]
 declare Bex_def[code_pred_inline]
 
-section {* Set operations *}
-
-declare eq_reflection[OF empty_def, code_pred_inline]
-
-declare subset_iff[code_pred_inline]
-
-declare Int_def[code_pred_inline]
-declare eq_reflection[OF Un_def, code_pred_inline]
-declare eq_reflection[OF UNION_eq, code_pred_inline]
+section {* Operations on Predicates *}
 
 lemma Diff[code_pred_inline]:
   "(A - B) = (%x. A x \<and> \<not> B x)"
@@ -51,7 +43,6 @@
   "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
   by (auto simp add: fun_eq_iff)
 
-
 section {* Setup for Numerals *}
 
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}