author | nipkow |
Thu, 12 Mar 1998 12:48:49 +0100 | |
changeset 4739 | 50457d3b80e2 |
parent 4738 | 699a91d01d6d |
child 4740 | 0136b5bbe9fe |
--- 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);