# HG changeset patch
# User wenzelm
# Date 856184064 -3600
# Node ID 9d3a3e62bf34c93a3f8b73e75fde92d79181479c
# Parent  2fa0f0c1c750681669d9aa681b6cce1c7ed641d9
mk_rews: automatically includes strip_shyps, zero_var_indexes;

diff -r 2fa0f0c1c750 -r 9d3a3e62bf34 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Mon Feb 17 13:26:32 1997 +0100
+++ b/src/Provers/simplifier.ML	Mon Feb 17 13:54:24 1997 +0100
@@ -185,8 +185,8 @@
 
 fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
 	      finish_tac, unsafe_finish_tac}) setmksimps mk_simps =
-  make_ss (Thm.set_mk_rews (mss, mk_simps), simps, procs, congs,
-    subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
+  make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
+    simps, procs, congs, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
 
 fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, 
 	      finish_tac, unsafe_finish_tac}) settermless termless =