# HG changeset patch
# User nipkow
# Date 889703329 -3600
# Node ID 50457d3b80e2d7cc5eca5be907f1f0e91d1d3378
# Parent  699a91d01d6da3a48f56e2eb65a232a92c0d55a8
Used merge_alists for loopers.

diff -r 699a91d01d6d -r 50457d3b80e2 src/Provers/simplifier.ML
--- 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);