Merging the meta-simplifier with the Provers-simplifier. Next step:
make the simplification procedure simpset-aware.

--- a/src/Provers/simplifier.ML	Thu Jun 24 17:54:53 2004 +0200
+++ b/src/Provers/simplifier.ML	Fri Jun 25 14:30:55 2004 +0200
@@ -6,19 +6,14 @@
 for the actual meta-level rewriting engine.
 *)
 
-infix 4
-  setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
-  addSolver addsimps delsimps addeqcongs deleqcongs addcongs delcongs
-  setmksimps setmkeqTrue setmkcong setmksym settermless addsimprocs delsimprocs;
-
 signature BASIC_SIMPLIFIER =
 sig
-  type simproc
+  type simproc = MetaSimplifier.simproc
   val mk_simproc: string -> cterm list
     -> (Sign.sg -> thm list -> term -> thm option) -> simproc
-  type solver
+  type solver = MetaSimplifier.solver
   val mk_solver: string -> (thm list -> int -> tactic) -> solver
-  type simpset
+  type simpset = MetaSimplifier.simpset
   val empty_ss: simpset
   val rep_ss: simpset ->
    {mss: MetaSimplifier.meta_simpset,
@@ -121,195 +116,8 @@
 structure Simplifier: SIMPLIFIER =
 struct
 
-
-(** simplification procedures **)
-
-(* datatype simproc *)
-
-datatype simproc =
-  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
-
-fun mk_simproc name lhss proc =
-  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
-
-fun simproc sg name ss =
-  mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
-fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg);
-
-fun rep_simproc (Simproc args) = args;
-
-
-
-(** solvers **)
-
-datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
-
-fun mk_solver name solver = Solver (name, solver, stamp());
-fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
-
-val merge_solvers = gen_merge_lists eq_solver;
-
-fun app_sols [] _ _ = no_tac
-  | app_sols (Solver(_,solver,_)::sols) thms i =
-       solver thms i ORELSE app_sols sols thms i;
-
-
-
-(** simplification sets **)
-
-(* type simpset *)
-
-datatype simpset =
-  Simpset of {
-    mss: MetaSimplifier.meta_simpset,
-    mk_cong: thm -> thm,
-    subgoal_tac: simpset -> int -> tactic,
-    loop_tacs: (string * (int -> tactic)) list,
-    unsafe_solvers: solver list,
-    solvers: solver list};
-
-fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
-  Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
-    loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
-
-val empty_ss =
-  let val mss = MetaSimplifier.set_mk_sym (MetaSimplifier.empty_mss, Some o symmetric_fun)
-  in make_ss mss I (K (K no_tac)) [] [] [] end;
-
-fun rep_ss (Simpset args) = args;
-fun prems_of_ss (Simpset {mss, ...}) = MetaSimplifier.prems_of_mss mss;
-
-
-(* print simpsets *)
-
-fun print_ss ss =
-  let
-    val Simpset {mss, ...} = ss;
-    val {simps, procs, congs} = MetaSimplifier.dest_mss mss;
-
-    val pretty_thms = map Display.pretty_thm;
-    fun pretty_proc (name, lhss) =
-      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
-  in
-    [Pretty.big_list "simplification rules:" (pretty_thms simps),
-      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
-      Pretty.big_list "congruences:" (pretty_thms congs)]
-    |> Pretty.chunks |> Pretty.writeln
-  end;
-
-
-(* extend simpsets *)
-
-fun (Simpset {mss, mk_cong, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
-    setsubgoaler subgoal_tac =
-  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
-    setloop tac =
-  make_ss mss mk_cong subgoal_tac [("", tac)] unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    addloop tac = make_ss mss mk_cong subgoal_tac
-      (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
-        warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac))
-      unsafe_solvers solvers;
-
-fun (ss as Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
- delloop name =
-  let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
-    if null del then (warning ("No such looper in simpset: " ^ name); ss)
-    else make_ss mss mk_cong subgoal_tac rest unsafe_solvers solvers
-  end;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...})
-    setSSolver solver =
-  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers [solver];
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    addSSolver sol =
-  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers (merge_solvers solvers [sol]);
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
-    setSolver unsafe_solver =
-  make_ss mss mk_cong subgoal_tac loop_tacs [unsafe_solver] solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    addSolver sol =
-  make_ss mss mk_cong subgoal_tac loop_tacs (merge_solvers unsafe_solvers [sol]) solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    setmksimps mk_simps =
-  make_ss (MetaSimplifier.set_mk_rews (mss, mk_simps)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    setmkeqTrue mk_eq_True =
-  make_ss (MetaSimplifier.set_mk_eq_True (mss, mk_eq_True)) mk_cong subgoal_tac loop_tacs
-    unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong = _, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    setmkcong mk_cong =
-  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    setmksym mksym =
-  make_ss (MetaSimplifier.set_mk_sym (mss, mksym)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
-    settermless termless =
-  make_ss (MetaSimplifier.set_termless (mss, termless)) mk_cong subgoal_tac loop_tacs
-    unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    addsimps rews =
-  make_ss (MetaSimplifier.add_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    delsimps rews =
-  make_ss (MetaSimplifier.del_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    addeqcongs newcongs =
-  make_ss (MetaSimplifier.add_congs (mss, newcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (Simpset {mss, subgoal_tac, mk_cong, loop_tacs, unsafe_solvers, solvers})
-    deleqcongs oldcongs =
-  make_ss (MetaSimplifier.del_congs (mss, oldcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-
-fun (ss as Simpset {mk_cong, ...}) addcongs newcongs =
-  ss addeqcongs map mk_cong newcongs;
-
-fun (ss as Simpset {mk_cong, ...}) delcongs oldcongs =
-  ss deleqcongs map mk_cong oldcongs;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    addsimprocs simprocs =
-  make_ss (MetaSimplifier.add_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac loop_tacs
-    unsafe_solvers solvers;
-
-fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
-    delsimprocs simprocs =
-  make_ss (MetaSimplifier.del_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac
-    loop_tacs unsafe_solvers solvers;
-
-fun clear_ss (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
-  make_ss (MetaSimplifier.clear_mss mss) mk_cong subgoal_tac [] unsafe_solvers solvers;
-
-
-(* merge simpsets *)
-
-(*ignores subgoal_tac of 2nd simpset!*)
-
-fun merge_ss
-   (Simpset {mss = mss1, mk_cong, loop_tacs = loop_tacs1, subgoal_tac,
-             unsafe_solvers = unsafe_solvers1, solvers = solvers1},
-    Simpset {mss = mss2, mk_cong = _, loop_tacs = loop_tacs2, subgoal_tac = _,
-             unsafe_solvers = unsafe_solvers2, solvers = solvers2}) =
-  make_ss (MetaSimplifier.merge_mss (mss1, mss2)) mk_cong subgoal_tac
-    (merge_alists loop_tacs1 loop_tacs2)
-    (merge_solvers unsafe_solvers1 unsafe_solvers2)
-    (merge_solvers solvers1 solvers2);
-
-
+(* Compatibility *)
+open MetaSimplifier;
 
 (** global and local simpset data **)
 
@@ -399,31 +207,6 @@
 val cong_del_local = change_local_ss (op delcongs);
 
 
-
-(** simplification tactics **)
-
-fun solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers) mss =
-  let
-    val ss =
-      make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers unsafe_solvers;
-    val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
-  in DEPTH_SOLVE solve1_tac end;
-
-fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
-
-(*note: may instantiate unknowns that appear also in other subgoals*)
-fun generic_simp_tac safe mode =
-  fn (Simpset {mss, mk_cong, 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 (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
-          mss i
-        THEN (solvs (MetaSimplifier.prems_of_mss mss) i ORELSE
-              TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
-    in simp_loop_tac end;
-
 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);
@@ -432,6 +215,7 @@
 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;
 fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
@@ -439,20 +223,6 @@
 fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
 
-
-
-(** simplification rules and conversions **)
-
-fun simp rew mode
-     (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
-  let
-    val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
-    fun prover m th = apsome fst (Seq.pull (tacf m th));
-  in rew mode prover mss thm end;
-
-val simp_thm = simp MetaSimplifier.rewrite_thm;
-val simp_cterm = simp MetaSimplifier.rewrite_cterm;
-
 val          simplify = simp_thm (false, false, false);
 val      asm_simplify = simp_thm (false, true, false);
 val     full_simplify = simp_thm (true, false, false);

--- a/src/Pure/ROOT.ML	Thu Jun 24 17:54:53 2004 +0200
+++ b/src/Pure/ROOT.ML	Fri Jun 25 14:30:55 2004 +0200
@@ -45,9 +45,9 @@
 use "fact_index.ML";
 use "pure_thy.ML";
 use "drule.ML";
-use "meta_simplifier.ML";
 use "tctical.ML";
 use "search.ML";
+use "meta_simplifier.ML";
 use "tactic.ML";
 
 (*proof term operations*)

--- a/src/Pure/meta_simplifier.ML	Thu Jun 24 17:54:53 2004 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Jun 25 14:30:55 2004 +0200
@@ -5,6 +5,11 @@
 Meta-level Simplification.
 *)
 
+infix 4
+  setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
+  addSolver addsimps delsimps addeqcongs deleqcongs addcongs delcongs
+  setmksimps setmkeqTrue setmkcong setmksym settermless addsimprocs delsimprocs;
+
 signature BASIC_META_SIMPLIFIER =
 sig
   val trace_simp: bool ref
@@ -12,12 +17,63 @@
   val simp_depth_limit: int ref
 end;
 
+signature AUX_SIMPLIFIER =
+sig
+  type meta_simpset
+  type simproc
+  val mk_simproc: string -> cterm list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+  type solver
+  val mk_solver: string -> (thm list -> int -> tactic) -> solver
+  type simpset
+  val empty_ss: simpset
+  val rep_ss: simpset ->
+   {mss: meta_simpset,
+    mk_cong: thm -> thm,
+    subgoal_tac: simpset -> int -> tactic,
+    loop_tacs: (string * (int -> tactic)) list,
+    unsafe_solvers: solver list,
+    solvers: solver list};
+  val print_ss: simpset -> unit
+  val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
+  val setloop:      simpset *             (int -> tactic) -> simpset
+  val addloop:      simpset *  (string * (int -> tactic)) -> simpset
+  val delloop:      simpset *   string                    -> simpset
+  val setSSolver:   simpset * solver -> simpset
+  val addSSolver:   simpset * solver -> simpset
+  val setSolver:    simpset * solver -> simpset
+  val addSolver:    simpset * solver -> simpset
+  val setmksimps:   simpset * (thm -> thm list) -> simpset
+  val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
+  val setmkcong:    simpset * (thm -> thm) -> simpset
+  val setmksym:     simpset * (thm -> thm option) -> simpset
+  val settermless:  simpset * (term * term -> bool) -> simpset
+  val addsimps:     simpset * thm list -> simpset
+  val delsimps:     simpset * thm list -> simpset
+  val addeqcongs:   simpset * thm list -> simpset
+  val deleqcongs:   simpset * thm list -> simpset
+  val addcongs:     simpset * thm list -> simpset
+  val delcongs:     simpset * thm list -> simpset
+  val addsimprocs:  simpset * simproc list -> simpset
+  val delsimprocs:  simpset * simproc list -> simpset
+  val merge_ss:     simpset * simpset -> simpset
+  val prems_of_ss:  simpset -> thm list
+  val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
+  val simproc: Sign.sg -> string -> string list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+  val simproc_i: Sign.sg -> string -> term list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+  val clear_ss  : simpset -> simpset
+  val simp_thm  : bool * bool * bool -> simpset -> thm -> thm
+  val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm
+end;
+
 signature META_SIMPLIFIER =
 sig
   include BASIC_META_SIMPLIFIER
+  include AUX_SIMPLIFIER
   exception SIMPLIFIER of string * thm
   exception SIMPROC_FAIL of string * exn
-  type meta_simpset
   val dest_mss          : meta_simpset ->
     {simps: thm list, congs: thm list, procs: (string * cterm list) list}
   val empty_mss         : meta_simpset
@@ -55,6 +111,9 @@
                           -> (meta_simpset -> thm -> thm option)
                           -> meta_simpset -> int -> thm -> thm
   val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
+  val asm_rewrite_goal_tac: bool*bool*bool ->
+    (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
+
 end;
 
 structure MetaSimplifier : META_SIMPLIFIER =
@@ -122,7 +181,7 @@
        in which case there is nothing better to do.
 *)
 type cong = {thm: thm, lhs: cterm};
-type simproc =
+type meta_simproc =
  {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
 
 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
@@ -134,7 +193,7 @@
 fun eq_prem (thm1, thm2) =
   #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
 
-fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
+fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
 
 fun mk_simproc (name, proc, lhs, id) =
   {name = name, proc = proc, lhs = lhs, id = id};
@@ -164,7 +223,7 @@
   Mss of {
     rules: rrule Net.net,
     congs: (string * cong) list * string list,
-    procs: simproc Net.net,
+    procs: meta_simproc Net.net,
     bounds: string list,
     prems: thm list,
     mk_rews: {mk: thm -> thm list,
@@ -528,6 +587,193 @@
 
 
 
+(** simplification procedures **)
+
+(* datatype simproc *)
+
+datatype simproc =
+  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
+
+fun mk_simproc name lhss proc =
+  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
+
+fun simproc sg name ss =
+  mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
+fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg);
+
+fun rep_simproc (Simproc args) = args;
+
+
+
+(** solvers **)
+
+datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
+
+fun mk_solver name solver = Solver (name, solver, stamp());
+fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
+
+val merge_solvers = gen_merge_lists eq_solver;
+
+fun app_sols [] _ _ = no_tac
+  | app_sols (Solver(_,solver,_)::sols) thms i =
+       solver thms i ORELSE app_sols sols thms i;
+
+
+
+(** simplification sets **)
+
+(* type simpset *)
+
+datatype simpset =
+  Simpset of {
+    mss: meta_simpset,
+    mk_cong: thm -> thm,
+    subgoal_tac: simpset -> int -> tactic,
+    loop_tacs: (string * (int -> tactic)) list,
+    unsafe_solvers: solver list,
+    solvers: solver list};
+
+fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
+  Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
+    loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
+
+val empty_ss =
+  let val mss = set_mk_sym (empty_mss, Some o symmetric_fun)
+  in make_ss mss I (K (K no_tac)) [] [] [] end;
+
+fun rep_ss (Simpset args) = args;
+fun prems_of_ss (Simpset {mss, ...}) = prems_of_mss mss;
+
+
+(* print simpsets *)
+
+fun print_ss ss =
+  let
+    val Simpset {mss, ...} = ss;
+    val {simps, procs, congs} = dest_mss mss;
+
+    val pretty_thms = map Display.pretty_thm;
+    fun pretty_proc (name, lhss) =
+      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
+  in
+    [Pretty.big_list "simplification rules:" (pretty_thms simps),
+      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
+      Pretty.big_list "congruences:" (pretty_thms congs)]
+    |> Pretty.chunks |> Pretty.writeln
+  end;
+
+
+(* extend simpsets *)
+
+fun (Simpset {mss, mk_cong, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
+    setsubgoaler subgoal_tac =
+  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
+    setloop tac =
+  make_ss mss mk_cong subgoal_tac [("", tac)] unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    addloop tac = make_ss mss mk_cong subgoal_tac
+      (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
+        warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac))
+      unsafe_solvers solvers;
+
+fun (ss as Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+ delloop name =
+  let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
+    if null del then (warning ("No such looper in simpset: " ^ name); ss)
+    else make_ss mss mk_cong subgoal_tac rest unsafe_solvers solvers
+  end;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...})
+    setSSolver solver =
+  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers [solver];
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    addSSolver sol =
+  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers (merge_solvers solvers [sol]);
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
+    setSolver unsafe_solver =
+  make_ss mss mk_cong subgoal_tac loop_tacs [unsafe_solver] solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    addSolver sol =
+  make_ss mss mk_cong subgoal_tac loop_tacs (merge_solvers unsafe_solvers [sol]) solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    setmksimps mk_simps =
+  make_ss (set_mk_rews (mss, mk_simps)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    setmkeqTrue mk_eq_True =
+  make_ss (set_mk_eq_True (mss, mk_eq_True)) mk_cong subgoal_tac loop_tacs
+    unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong = _, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    setmkcong mk_cong =
+  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    setmksym mksym =
+  make_ss (set_mk_sym (mss, mksym)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
+    settermless termless =
+  make_ss (set_termless (mss, termless)) mk_cong subgoal_tac loop_tacs
+    unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    addsimps rews =
+  make_ss (add_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    delsimps rews =
+  make_ss (del_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    addeqcongs newcongs =
+  make_ss (add_congs (mss, newcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, subgoal_tac, mk_cong, loop_tacs, unsafe_solvers, solvers})
+    deleqcongs oldcongs =
+  make_ss (del_congs (mss, oldcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (ss as Simpset {mk_cong, ...}) addcongs newcongs =
+  ss addeqcongs map mk_cong newcongs;
+
+fun (ss as Simpset {mk_cong, ...}) delcongs oldcongs =
+  ss deleqcongs map mk_cong oldcongs;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    addsimprocs simprocs =
+  make_ss (add_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac loop_tacs
+    unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+    delsimprocs simprocs =
+  make_ss (del_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac
+    loop_tacs unsafe_solvers solvers;
+
+fun clear_ss (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
+  make_ss (clear_mss mss) mk_cong subgoal_tac [] unsafe_solvers solvers;
+
+
+(* merge simpsets *)
+
+(*ignores subgoal_tac of 2nd simpset!*)
+
+fun merge_ss
+   (Simpset {mss = mss1, mk_cong, loop_tacs = loop_tacs1, subgoal_tac,
+             unsafe_solvers = unsafe_solvers1, solvers = solvers1},
+    Simpset {mss = mss2, mk_cong = _, loop_tacs = loop_tacs2, subgoal_tac = _,
+             unsafe_solvers = unsafe_solvers2, solvers = solvers2}) =
+  make_ss (merge_mss (mss1, mss2)) mk_cong subgoal_tac
+    (merge_alists loop_tacs1 loop_tacs2)
+    (merge_solvers unsafe_solvers1 unsafe_solvers2)
+    (merge_solvers solvers1 solvers2);
+
 (** rewriting **)
 
 (*
@@ -666,7 +912,7 @@
                                      else sort rrs (re1,rr::re2)
     in sort rrs ([],[]) end
 
-    fun proc_rews ([]:simproc list) = None
+    fun proc_rews ([]:meta_simproc list) = None
       | proc_rews ({name, proc, lhs, ...} :: ps) =
           if Pattern.matches tsigt (term_of lhs, term_of t) then
             (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
@@ -965,6 +1211,47 @@
 fun rewrite_term sg rules procs =
   Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
 
+(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
+fun asm_rewrite_goal_tac mode prover_tac mss =
+  SELECT_GOAL
+    (PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) mss 1));
+
+(** simplification tactics **)
+
+fun solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers) mss =
+  let
+    val ss =
+      make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers unsafe_solvers;
+    val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
+  in DEPTH_SOLVE solve1_tac end;
+
+fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
+
+(*note: may instantiate unknowns that appear also in other subgoals*)
+fun generic_simp_tac safe mode =
+  fn (Simpset {mss, mk_cong, 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 (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
+          mss i
+        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;
+
+(** simplification rules and conversions **)
+
+fun simp rew mode
+     (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
+  let
+    val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
+    fun prover m th = apsome fst (Seq.pull (tacf m th));
+  in rew mode prover mss thm end;
+
+val simp_thm = simp rewrite_thm;
+val simp_cterm = simp rewrite_cterm;
+
 end;
 
 structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;

--- a/src/Pure/tactic.ML	Thu Jun 24 17:54:53 2004 +0200
+++ b/src/Pure/tactic.ML	Fri Jun 25 14:30:55 2004 +0200
@@ -9,8 +9,6 @@
 signature BASIC_TACTIC =
 sig
   val ares_tac          : thm list -> int -> tactic
-  val asm_rewrite_goal_tac: bool*bool*bool ->
-    (MetaSimplifier.meta_simpset -> tactic) -> MetaSimplifier.meta_simpset -> int -> tactic
   val assume_tac        : int -> tactic
   val atac      : int ->tactic
   val bimatch_from_nets_tac:
@@ -74,8 +72,6 @@
   val net_resolve_tac   : thm list -> int -> tactic
   val norm_hhf_rule     : thm -> thm
   val norm_hhf_tac      : int -> tactic
-  val PRIMITIVE         : (thm -> thm) -> tactic
-  val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic
   val prune_params_tac  : tactic
   val rename_params_tac : string list -> int -> tactic
   val rename_tac        : string -> int -> tactic
@@ -137,12 +133,6 @@
 
 (*** Basic tactics ***)
 
-(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
-fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
-
-(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
-fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
-
 (*** The following fail if the goal number is out of range:
      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
 
@@ -499,24 +489,16 @@
 
 (*** Meta-Rewriting Tactics ***)
 
-fun result1 tacf mss thm =
-  apsome fst (Seq.pull (tacf mss thm));
-
 val simple_prover =
-  result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
+  SINGLE o (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
 
 val rewrite = MetaSimplifier.rewrite_aux simple_prover;
 val simplify = MetaSimplifier.simplify_aux simple_prover;
 val rewrite_rule = simplify true;
 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
 
-(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
-fun asm_rewrite_goal_tac mode prover_tac mss =
-  SELECT_GOAL
-    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (result1 prover_tac) mss 1));
-
 fun rewrite_goal_tac rews =
-  asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
+  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
 
 (*Rewrite throughout proof state. *)
 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);

--- a/src/Pure/tctical.ML	Thu Jun 24 17:54:53 2004 +0200
+++ b/src/Pure/tctical.ML	Fri Jun 25 14:30:55 2004 +0200
@@ -39,6 +39,8 @@
   val ORELSE'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val pause_tac         : tactic
   val print_tac         : string -> tactic
+  val PRIMITIVE         : (thm -> thm) -> tactic
+  val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic
   val RANGE             : (int -> tactic) list -> int -> tactic
   val REPEAT            : tactic -> tactic
   val REPEAT1           : tactic -> tactic
@@ -51,6 +53,7 @@
   val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
   val DETERM_UNTIL      : (thm -> bool) -> tactic -> tactic
   val SELECT_GOAL       : tactic -> int -> tactic
+  val SINGLE            : tactic -> thm -> thm option
   val SOMEGOAL          : (int -> tactic) -> tactic
   val strip_context     : term -> (string * typ) list * term list * term
   val SUBGOAL           : ((term*int) -> tactic) -> int -> tactic
@@ -491,6 +494,15 @@
 
 fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf);
 
+(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
+fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
+
+(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
+fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
+
+(* Inverse (more or less) of PRIMITIVE *)
+fun SINGLE tacf = apsome fst o Seq.pull o tacf
+		  
 end;
 
 open Tactical;