canonical merge operations

--- a/src/Pure/Proof/extraction.ML	Mon Apr 16 12:16:11 2007 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Apr 16 16:11:03 2007 +0200
@@ -204,7 +204,7 @@
        realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
     {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
      typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
-     types = merge_alists types1 types2,
+     types = AList.merge (op =) (K true) (types1, types2),
      realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
      defs = Library.merge Thm.eq_thm (defs1, defs2),
      expand = Library.merge (op =) (expand1, expand2),
@@ -343,7 +343,7 @@
     val thy' = add_syntax thy;
     val {realizes_eqns, typeof_eqns, defs, types, ...} =
       ExtractionData.get thy';
-    val procs = maps (fst o snd) types;
+    val procs = maps (rev o fst o snd) types;
     val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
     val prop' = Pattern.rewrite_term thy'
       (map (Logic.dest_equals o prop_of) defs) [] prop;
@@ -390,14 +390,12 @@
 (** types with computational content **)
 
 fun add_types tys thy =
-  let val {realizes_eqns, typeof_eqns, types, realizers,
-    defs, expand, prep} = ExtractionData.get thy;
-  in
-    ExtractionData.put
+  ExtractionData.map
+    (fn {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =>
       {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
-       types = map (apfst (Sign.intern_type thy)) tys @ types,
-       realizers = realizers, defs = defs, expand = expand, prep = prep} thy
-  end;
+       types = fold (AList.update (op =) o apfst (Sign.intern_type thy)) tys types,
+       realizers = realizers, defs = defs, expand = expand, prep = prep})
+    thy;
 
 
 (** Pure setup **)
@@ -460,7 +458,7 @@
     val thy' = add_syntax thy;
     val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
       ExtractionData.get thy;
-    val procs = maps (fst o snd) types;
+    val procs = maps (rev o fst o snd) types;
     val rtypes = map fst types;
     val typroc = typeof_proc (Sign.defaultS thy');
     val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o

--- a/src/Pure/meta_simplifier.ML	Mon Apr 16 12:16:11 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Apr 16 16:11:03 2007 +0200
@@ -247,7 +247,6 @@
 fun solver_name (Solver {name, ...}) = name;
 fun solver ss (Solver {solver = tac, ...}) = tac ss;
 fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
-val merge_solvers = gen_merge_lists eq_solver;
 
 
 (* diagnostics *)
@@ -742,7 +741,7 @@
 
 fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
-    subgoal_tac, loop_tacs, (unsafe_solvers, merge_solvers solvers [solver])));
+    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
 
 fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
@@ -750,7 +749,7 @@
 
 fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
-    subgoal_tac, loop_tacs, (merge_solvers unsafe_solvers [solver], solvers)));
+    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
 
 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
   subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
@@ -795,8 +794,8 @@
     val weak' = merge (op =) (weak1, weak2);
     val procs' = Net.merge eq_proc (procs1, procs2);
     val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
-    val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2;
-    val solvers' = merge_solvers solvers1 solvers2;
+    val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
+    val solvers' = merge eq_solver (solvers1, solvers2);
   in
     make_simpset ((rules', prems', bounds', NONE), ((congs', weak'), procs',
       mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))

--- a/src/Pure/simplifier.ML	Mon Apr 16 12:16:11 2007 +0200
+++ b/src/Pure/simplifier.ML	Mon Apr 16 16:11:03 2007 +0200
@@ -274,7 +274,7 @@
     val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
     val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
     val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
-      (if safe then solvers else unsafe_solvers));
+      (rev (if safe then solvers else unsafe_solvers)));
 
     fun simp_loop_tac i =
       Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
@@ -286,7 +286,7 @@
 fun simp rew mode ss thm =
   let
     val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
-    val tacf = solve_all_tac unsafe_solvers;
+    val tacf = solve_all_tac (rev unsafe_solvers);
     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   in rew mode prover ss thm end;