src/Pure/meta_simplifier.ML

 fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
 
 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 *)
 
 exception SIMPLIFIER of string * thm;

   subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
     (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
 
 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,
     subgoal_tac, loop_tacs, ([solver], solvers)));
 
 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,
   subgoal_tac, loop_tacs, (solvers, solvers)));
 

     val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
     val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
     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')))
   end;