--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 23 14:50:13 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Sep 23 14:50:14 2010 +0200
@@ -2316,9 +2316,8 @@
(all_input_of T))
preds
in
- (* remove not_False_eq_True when simpset in prove_match is better *)
simp_tac (HOL_basic_ss addsimps
- (@{thms HOL.simp_thms} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1
+ (@{thms HOL.simp_thms} @ (@{thm eval_pred} :: defs))) 1
(* need better control here! *)
end