| changeset 4739 | 50457d3b80e2 |
| parent 4722 | d2e44673c21e |
| child 4741 | 7fcd106cb0ed |
--- a/src/Provers/simplifier.ML Thu Mar 12 10:40:08 1998 +0100 +++ b/src/Provers/simplifier.ML Thu Mar 12 12:48:49 1998 +0100 @@ -240,7 +240,7 @@ subgoal_tac, finish_tac, unsafe_finish_tac}, Simpset {mss = mss2, loop_tacs = loop_tacs2, ...}) = make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac, - foldl overwrite (loop_tacs1,loop_tacs2), + merge_alists loop_tacs1 loop_tacs2, finish_tac, unsafe_finish_tac);