src/Provers/simplifier.ML
changeset 12282 f98beaaa7c4f
parent 12109 bd6eb9194a5d
child 12311 ce5f9e61c037
--- 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 =