# HG changeset patch
# User oheimb
# Date 934818254 -7200
# Node ID 3af1e69b25b85b3c0c60e13a5ae6f452178c5968
# Parent  7ee4eecdc8a663aa13d70cfc9b7d580f3e5c7627
forgot to write back adaption of onlysimps

diff -r 7ee4eecdc8a6 -r 3af1e69b25b8 src/Provers/simplifier.ML
--- 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;