# HG changeset patch
# User bulwahn
# Date 1285246214 -7200
# Node ID 7186d338f2e12e8ab439d3045c4f4b12532c3024
# Parent  655307cb8489cd5ed236589f1e71633f16e24290
removing duplicate rewrite rule from simpset in predicate compiler

diff -r 655307cb8489 -r 7186d338f2e1 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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