mk_rews: automatically includes strip_shyps, zero_var_indexes;
authorwenzelm
Mon Feb 17 13:54:24 1997 +0100 (1997-02-17)
changeset 26459d3a3e62bf34
parent 2644 2fa0f0c1c750
child 2646 099a9155f608
mk_rews: automatically includes strip_shyps, zero_var_indexes;
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/simplifier.ML	Mon Feb 17 13:26:32 1997 +0100
     1.2 +++ b/src/Provers/simplifier.ML	Mon Feb 17 13:54:24 1997 +0100
     1.3 @@ -185,8 +185,8 @@
     1.4  
     1.5  fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
     1.6  	      finish_tac, unsafe_finish_tac}) setmksimps mk_simps =
     1.7 -  make_ss (Thm.set_mk_rews (mss, mk_simps), simps, procs, congs,
     1.8 -    subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
     1.9 +  make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
    1.10 +    simps, procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
    1.11  
    1.12  fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
    1.13  	      finish_tac, unsafe_finish_tac}) settermless termless =