src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 44928 7ef6505bde7f
parent 44890 22f665a2e91c
child 45970 b6d0cff57d96
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 14 10:08:52 2011 -0400
@@ -1017,7 +1017,7 @@
 code_pred [inductify] Image .
 thm Image.equation
 declare singleton_iff[code_pred_inline]
-declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
+declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]
 
 code_pred (expected_modes:
   (o => bool) => o => bool,