src/Provers/simplifier.ML

     delsimprocs simprocs =
   make_ss
     (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;
 
 
 (* merge simpsets *)    (*NOTE: ignores tactics of 2nd simpset (except loopers)*)