# HG changeset patch
# User bulwahn
# Date 1253715612 -7200
# Node ID ffe062d9ae95cdfe7dc8309a6402144eaef6bc46
# Parent  3bd9296b16acd57103b694d1c8736aa7e167493b
modified handling of side conditions in proof procedure of predicate compiler

diff -r 3bd9296b16ac -r ffe062d9ae95 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 13:48:16 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -108,7 +108,7 @@
 
 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
 
-fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
+fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
 fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
 
 val do_proofs = ref true;
@@ -1328,7 +1328,7 @@
   end;
   
 (* special setup for simpset *)                  
-val HOL_basic_ss' = HOL_basic_ss setSolver 
+val HOL_basic_ss' = HOL_basic_ss addsimps @{thms "HOL.simp_thms"} setSolver 
   (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
 
 (* Definition of executable functions and their intro and elim rules *)
@@ -1576,7 +1576,8 @@
         preds
   in 
     (* remove not_False_eq_True when simpset in prove_match is better *)
-    simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 
+    simp_tac (HOL_basic_ss addsimps
+      (@{thms "HOL.simp_thms"} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
     (* need better control here! *)
   end