# HG changeset patch
# User wenzelm
# Date 869045682 -7200
# Node ID 5b5807645a1a78b6ef8015086c4ce205743f2202
# Parent  ab0a9fbed4c027f2a2b6c9c2d459f5788486e4d4
fixed merge of internal simprocs;

diff -r ab0a9fbed4c0 -r 5b5807645a1a src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Mon Jul 14 12:47:21 1997 +0200
+++ b/src/Provers/simplifier.ML	Wed Jul 16 11:34:42 1997 +0200
@@ -247,9 +247,11 @@
   let
     val simps' = gen_union eq_thm (simps, simps2);
     val procs' = gen_union eq_simproc (procs, procs2);
+    val meta_procs' = flat (map (fn Simproc {procs, ...} => procs) procs');
     val congs' = gen_union eq_thm (congs, congs2);
     val mss' = Thm.set_mk_rews (empty_mss, Thm.mk_rews_of_mss mss);
     val mss' = Thm.add_simps (mss', simps');
+    val mss' = Thm.add_simprocs (mss', meta_procs');
     val mss' = Thm.add_congs (mss', congs');
   in
     make_ss (mss', simps', procs', congs', subgoal_tac, loop_tac,