--- a/src/Provers/simplifier.ML Wed Sep 29 14:35:18 1999 +0200
+++ b/src/Provers/simplifier.ML Wed Sep 29 14:36:04 1999 +0200
@@ -210,8 +210,7 @@
fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
setmksimps mk_simps =
- make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
- subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+ make_ss (Thm.set_mk_rews (mss, mk_simps), subgoal_tac, loop_tacs, unsafe_solvers, solvers);
fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
setmkeqTrue mk_eq_True =