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.
forgot to write back adaption of onlysimps
authoroheimb
Mon, 16 Aug 1999 17:44:14 +0200
changeset 7217 3af1e69b25b8
parent 7216 7ee4eecdc8a6
child 7218 bfa767b4dc51
forgot to write back adaption of onlysimps
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/simplifier.ML	Mon Aug 16 17:42:37 1999 +0200
+++ b/src/Provers/simplifier.ML	Mon Aug 16 17:44:14 1999 +0200
@@ -247,8 +247,8 @@
     (Thm.del_simprocs (mss, map rep_simproc simprocs),
       subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
 
-fun onlysimps (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}, rews) =
-  make_ss (Thm.clear_mss mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac)
+fun onlysimps (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}, rews) =
+  make_ss (Thm.clear_mss mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac)
     addsimps rews;
isabelle