src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 44928 7ef6505bde7f
parent 44890 22f665a2e91c
child 45231 d85a2fdc586c
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Sep 14 10:08:52 2011 -0400
@@ -41,7 +41,7 @@
 
 declare Int_def[code_pred_inline]
 declare eq_reflection[OF Un_def, code_pred_inline]
-declare eq_reflection[OF UNION_def, code_pred_inline]
+declare eq_reflection[OF UNION_eq, code_pred_inline]
 
 lemma Diff[code_pred_inline]:
   "(A - B) = (%x. A x \<and> \<not> B x)"