# HG changeset patch
# User wenzelm
# Date 853521597 -3600
# Node ID b7dd670cfe3a3fef89921e4779cad6ca8b7526fe
# Parent  aecaa76e7eff596c20f416e130f947b41c64c647
addsimps, addeqcongs: replaced @ by gen_union;

diff -r aecaa76e7eff -r b7dd670cfe3a src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Jan 17 16:58:59 1997 +0100
+++ b/src/Provers/simplifier.ML	Fri Jan 17 18:19:57 1997 +0100
@@ -161,7 +161,7 @@
 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac})
     addsimps rews =
   let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in
-    make_ss (Thm.add_simps (mss, rews'), rews' @ simps,
+    make_ss (Thm.add_simps (mss, rews'), gen_union eq_thm (rews', simps),
       procs, congs, subgoal_tac, finish_tac, loop_tac)
   end;
 
@@ -176,7 +176,8 @@
 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac})
     addeqcongs newcongs =
   make_ss (Thm.add_congs (mss, newcongs),
-    simps, procs, newcongs @ congs, subgoal_tac, finish_tac, loop_tac);
+    simps, procs, gen_union eq_thm (newcongs, congs),
+    subgoal_tac, finish_tac, loop_tac);
 
 fun addsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}),
       simproc as Simproc {name = _, procs = procs'}) =