export generic_simp_tac;

--- a/src/Provers/simplifier.ML	Tue May 16 14:07:49 2000 +0200
+++ b/src/Provers/simplifier.ML	Wed May 17 17:16:21 2000 +0200
@@ -60,6 +60,7 @@
   val Delsimps: thm list -> unit
   val Addsimprocs: simproc list -> unit
   val Delsimprocs: simproc list -> unit
+  val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
   val               simp_tac: simpset -> int -> tactic
   val           asm_simp_tac: simpset -> int -> tactic
   val          full_simp_tac: simpset -> int -> tactic
@@ -382,32 +383,27 @@
 
 fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
 
-(*unsafe: may instantiate unknowns that appear also in other subgoals*)
-fun basic_gen_simp_tac mode solvers =
-  fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) =>
+(*note: may instantiate unknowns that appear also in other subgoals*)
+fun generic_simp_tac safe mode =
+  fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
     let
+      val solvs = app_sols (if safe then solvers else unsafe_solvers);
       fun simp_loop_tac i =
         asm_rewrite_goal_tac mode
           (solve_all_tac (subgoal_tac,loop_tacs,unsafe_solvers))
           mss i
-        THEN (solvers (prems_of_mss mss) i ORELSE
+        THEN (solvs (prems_of_mss mss) i ORELSE
               TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
     in simp_loop_tac end;
 
-fun gen_simp_tac mode 
-      (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) =
-  basic_gen_simp_tac mode (app_sols unsafe_solvers) ss;
-
-val          simp_tac = gen_simp_tac (false, false, false);
-val      asm_simp_tac = gen_simp_tac (false, true, false);
-val     full_simp_tac = gen_simp_tac (true,  false, false);
-val   asm_lr_simp_tac = gen_simp_tac (true,  true, false);
-val asm_full_simp_tac = gen_simp_tac (true,  true, true);
+val          simp_tac = generic_simp_tac false (false, false, false);
+val      asm_simp_tac = generic_simp_tac false (false, true, false);
+val     full_simp_tac = generic_simp_tac false (true,  false, false);
+val   asm_lr_simp_tac = generic_simp_tac false (true,  true, false);
+val asm_full_simp_tac = generic_simp_tac false (true,  true, true);
 
 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
-fun safe_asm_full_simp_tac (ss as Simpset {mss, subgoal_tac, loop_tacs, 
-	unsafe_solvers, solvers}) = 
-  basic_gen_simp_tac (true, true, true) (app_sols solvers) ss;
+val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
 
 (*the abstraction over the proof state delays the dereferencing*)
 fun          Simp_tac i st =          simp_tac (simpset ()) i st;