--- 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;