src/HOL/ex/predicate_compile.ML
changeset 32659 ffe062d9ae95
parent 32351 96f9e6402403
child 32663 c2f63118b251
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 13:48:16 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5  fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
     1.6  
     1.7 -fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
     1.8 +fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
     1.9  fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
    1.10  
    1.11  val do_proofs = ref true;
    1.12 @@ -1328,7 +1328,7 @@
    1.13    end;
    1.14    
    1.15  (* special setup for simpset *)                  
    1.16 -val HOL_basic_ss' = HOL_basic_ss setSolver 
    1.17 +val HOL_basic_ss' = HOL_basic_ss addsimps @{thms "HOL.simp_thms"} setSolver 
    1.18    (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
    1.19  
    1.20  (* Definition of executable functions and their intro and elim rules *)
    1.21 @@ -1576,7 +1576,8 @@
    1.22          preds
    1.23    in 
    1.24      (* remove not_False_eq_True when simpset in prove_match is better *)
    1.25 -    simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 
    1.26 +    simp_tac (HOL_basic_ss addsimps
    1.27 +      (@{thms "HOL.simp_thms"} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
    1.28      (* need better control here! *)
    1.29    end
    1.30