# HG changeset patch
# User wenzelm
# Date 938608564 -7200
# Node ID 1ad3866b86cc450dd21bda1f5ca493ca2daa4795
# Parent  c67115c0e105b10e5ed18f63578f3aae37e1febb
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
  (asm_simp performance!);

diff -r c67115c0e105 -r 1ad3866b86cc src/Provers/simplifier.ML
--- 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 =