# HG changeset patch
# User wenzelm
# Date 1006617272 -3600
# Node ID f98beaaa7c4ff685f724100a6000ce9cd7799a54
# Parent  3bd113b8f7a6de1b5a124856e2190dfb86757dd9
generic_merge;

diff -r 3bd113b8f7a6 -r f98beaaa7c4f src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Sat Nov 24 16:54:10 2001 +0100
+++ b/src/Provers/simplifier.ML	Sat Nov 24 16:54:32 2001 +0100
@@ -134,11 +134,10 @@
 
 datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
 
-fun mk_solver name solver = Solver(name, solver, stamp());
+fun mk_solver name solver = Solver (name, solver, stamp());
+fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
 
-fun eq_solver (Solver(_,_,s1),Solver(_,_,s2)) = s1=s2;
-
-val merge_solvers = generic_merge eq_solver I I;
+val merge_solvers = gen_merge_lists eq_solver;
 
 fun app_sols [] _ _ = no_tac
   | app_sols (Solver(_,solver,_)::sols) thms i =