diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- 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 \ \ B x)"