src/Provers/simplifier.ML
changeset 2645 9d3a3e62bf34
parent 2629 b442786d4469
child 3520 5b5807645a1a
equal deleted inserted replaced
2644:2fa0f0c1c750 2645:9d3a3e62bf34
   183   make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac,
   183   make_ss (mss, simps, procs, congs, subgoal_tac, loop_tac,
   184     finish_tac, fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps);
   184     finish_tac, fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps);
   185 
   185 
   186 fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
   186 fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
   187 	      finish_tac, unsafe_finish_tac}) setmksimps mk_simps =
   187 	      finish_tac, unsafe_finish_tac}) setmksimps mk_simps =
   188   make_ss (Thm.set_mk_rews (mss, mk_simps), simps, procs, congs,
   188   make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
   189     subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   189     simps, procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   190 
   190 
   191 fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
   191 fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
   192 	      finish_tac, unsafe_finish_tac}) settermless termless =
   192 	      finish_tac, unsafe_finish_tac}) settermless termless =
   193   make_ss (Thm.set_termless (mss, termless), simps, procs, congs,
   193   make_ss (Thm.set_termless (mss, termless), simps, procs, congs,
   194     subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   194     subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);