# HG changeset patch
# User nipkow
# Date 937933867 -7200
# Node ID a9391550eea1a98b6b3d67914c2ba65d9fabad30
# Parent  1d9263172b54133389d08aca3208703a1bf3aba3
Mod because of new solver interface.

diff -r 1d9263172b54 -r a9391550eea1 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/FOL/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -325,8 +325,8 @@
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
                             addsimprocs [defALL_regroup,defEX_regroup]
-			    setSSolver   safe_solver
-			    setSolver  unsafe_solver
+			    setSSolver  (mk_solver "FOL safe" safe_solver)
+			    setSolver  (mk_solver "FOL unsafe" unsafe_solver)
 			    setmksimps (mksimps mksimps_pairs);
 
 
diff -r 1d9263172b54 -r a9391550eea1 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/Arith.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -1000,7 +1000,8 @@
 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
 solver all the time rather than add the additional check. *)
 
-simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac);
+simpset_ref () := (simpset() addSolver
+   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
 
 (* Elimination of `-' on nat due to John Harrison *)
 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
diff -r 1d9263172b54 -r a9391550eea1 src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/List.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -804,6 +804,7 @@
 by (exhaust_tac "na" 1);
  by Auto_tac;
 qed_spec_mp "take_take";
+Addsimps [take_take];
 
 Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
 by (induct_tac "m" 1);
@@ -811,6 +812,7 @@
 by (exhaust_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "drop_drop";
+Addsimps [drop_drop];
 
 Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
 by (induct_tac "m" 1);
diff -r 1d9263172b54 -r a9391550eea1 src/HOL/TLA/Memory/MemoryImplementation.ML
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -28,7 +28,7 @@
   let 
     val (cs,ss) = MI_css
   in
-    (cs addSEs [squareE], ss addSSolver (fn thms => assume_tac ORELSE' (etac notE)))
+    (cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
 end;
 
 val temp_elim = make_elim o temp_use;
diff -r 1d9263172b54 -r a9391550eea1 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/WF.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -260,7 +260,7 @@
     (cut_facts_tac hyps THEN'
        DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
                         eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss addSolver indhyp_tac;
+val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac);
 
 Goalw [is_recfun_def,cut_def]
     "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
diff -r 1d9263172b54 -r a9391550eea1 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOL/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -429,14 +429,18 @@
 
 fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
 
-fun unsafe_solver prems = FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems),
-				 atac         ,       etac  FalseE ];
+fun unsafe_solver_tac prems =
+  FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
+val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
+
 (*No premature instantiation of variables during simplification*)
-fun   safe_solver prems = FIRST'[  match_tac(reflexive_thm::TrueI::refl::prems),
-				 eq_assume_tac, ematch_tac [FalseE]];
+fun safe_solver_tac prems =
+  FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
+         eq_assume_tac, ematch_tac [FalseE]];
+val safe_solver = mk_solver "HOL safe" safe_solver_tac;
 
 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
-			    setSSolver   safe_solver
+			    setSSolver safe_solver
 			    setSolver  unsafe_solver
 			    setmksimps (mksimps mksimps_pairs)
 			    setmkeqTrue mk_eq_True;
diff -r 1d9263172b54 -r a9391550eea1 src/HOLCF/HOLCF.ML
--- a/src/HOLCF/HOLCF.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOLCF/HOLCF.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -8,7 +8,7 @@
 
 use"adm.ML";
 
-simpset_ref() := simpset() addSolver(fn thms =>
-            (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
+simpset_ref() := simpset() addSolver
+   (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
 
 val HOLCF_ss = simpset();
diff -r 1d9263172b54 -r a9391550eea1 src/HOLCF/Lift.ML
--- a/src/HOLCF/Lift.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/HOLCF/Lift.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -71,7 +71,8 @@
                   REPEAT (cont_tac i);
 
 
-simpset_ref() := simpset() addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+simpset_ref() := simpset() addSolver
+  (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
 
 
 
diff -r 1d9263172b54 -r a9391550eea1 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -277,7 +277,7 @@
         | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD))
         | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
         | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD))
-        | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp(prth(addthms (mk j1) (mk j2)))))
+        | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp((*prth*)(addthms (mk j1) (mk j2)))))
         | mk(Multiplied(n,j)) = ((*writeln"*";*)multn(n,mk j))
 
   in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end
diff -r 1d9263172b54 -r a9391550eea1 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/Sequents/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -241,8 +241,8 @@
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
-			   setSSolver   safe_solver
-			   setSolver    unsafe_solver
+			   setSSolver   (mk_solver "safe" safe_solver)
+			   setSolver    (mk_solver "unsafe" unsafe_solver)
 			   setmksimps   (map mk_meta_eq o atomize o gen_all);
 
 val LK_simps =
diff -r 1d9263172b54 -r a9391550eea1 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/Order.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -242,9 +242,9 @@
 
 (*Rewriting with bijections and converse (function inverse)*)
 val bij_inverse_ss = 
-    simpset() setSolver 
-      type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
-				       inj_is_fun, comp_fun, comp_bij])
+    simpset() setSolver (mk_solver ""
+      (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
+				        inj_is_fun, comp_fun, comp_bij])))
           addsimps [right_inverse_bij];
 
 Goalw [ord_iso_def] 
diff -r 1d9263172b54 -r a9391550eea1 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/Perm.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -344,8 +344,8 @@
 by (rtac lam_funtype 2);
 by (typecheck_tac (tcset() addTCs [prem]));
 by (asm_simp_tac (simpset() 
-                   setSolver 
-                   type_solver_tac (tcset() addTCs [prem, lam_funtype])) 1);
+                   setSolver (mk_solver ""
+                   (type_solver_tac (tcset() addTCs [prem, lam_funtype])))) 1);
 qed "comp_lam";
 
 Goal "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
@@ -353,8 +353,8 @@
     f_imp_injective 1);
 by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
 by (asm_simp_tac (simpset()  
-		  setSolver
-		  type_solver_tac (tcset() addTCs [inj_is_fun])) 1);
+		  setSolver (mk_solver ""
+		  (type_solver_tac (tcset() addTCs [inj_is_fun])))) 1);
 qed "comp_inj";
 
 Goalw [surj_def]
diff -r 1d9263172b54 -r a9391550eea1 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -335,9 +335,10 @@
        If the premises get simplified, then the proofs could fail.*)
      val min_ss = empty_ss
 	   setmksimps (map mk_eq o ZF_atomize o gen_all)
-	   setSolver  (fn prems => resolve_tac (triv_rls@prems) 
+	   setSolver (mk_solver "minimal"
+                      (fn prems => resolve_tac (triv_rls@prems) 
 				   ORELSE' assume_tac
-				   ORELSE' etac FalseE);
+				   ORELSE' etac FalseE));
 
      val quant_induct = 
 	 prove_goalw_cterm part_rec_defs 
diff -r 1d9263172b54 -r a9391550eea1 src/ZF/WF.ML
--- a/src/ZF/WF.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/WF.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -229,7 +229,7 @@
                         eresolve_tac [underD, transD, spec RS mp]));
 
 (*** NOTE! some simplifications need a different solver!! ***)
-val wf_super_ss = simpset() setSolver indhyp_tac;
+val wf_super_ss = simpset() setSolver (mk_solver "WF" indhyp_tac);
 
 Goalw [is_recfun_def]
     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
diff -r 1d9263172b54 -r a9391550eea1 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/ZF/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -107,6 +107,6 @@
 
 simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
                            addsplits [split_if]
-                           setSolver Type_solver_tac;
+                           setSolver (mk_solver "types" Type_solver_tac);
 
 val ZF_ss = simpset();