Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
authorwenzelm
Wed, 29 Sep 1999 14:36:04 +0200
changeset 7646 1ad3866b86cc
parent 7645 c67115c0e105
child 7647 2ceddd91cd0a
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes (asm_simp performance!);
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle