# HG changeset patch
# User wenzelm
# Date 1165529815 -3600
# Node ID 45e7491bea47e07d9eff68a38f446315c739249b
# Parent  dfc7b21d0ee90d1ca62796b089528a60a3063545
reorganized structure Tactic vs. MetaSimplifier;

diff -r dfc7b21d0ee9 -r 45e7491bea47 TFL/casesplit.ML
--- a/TFL/casesplit.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/TFL/casesplit.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -80,8 +80,8 @@
 functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
 struct
 
-val rulify_goals = Tactic.rewrite_goals_rule Data.rulify;
-val atomize_goals = Tactic.rewrite_goals_rule Data.atomize;
+val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
+val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
 
 (* beta-eta contract the theorem *)
 fun beta_eta_contract thm =
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Hyperreal/transfer.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -62,7 +62,7 @@
     val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
     val meta = LocalDefs.meta_rewrite_rule ctxt
     val unfolds' = map meta unfolds and refolds' = map meta refolds;
-    val (_$_$t') = concl_of (Tactic.rewrite true unfolds' (cterm_of thy t))
+    val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
     val u = unstar_term consts t'
     val tac =
       rewrite_goals_tac (ths @ refolds' @ unfolds') THEN
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Integ/presburger.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -56,7 +56,7 @@
 val powerarith =
     (map thm ["nat_number_of", "zpower_number_of_even",
               "zpower_Pls", "zpower_Min"]) @
-    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
+    [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
                            thm "one_eq_Numeral1_nring"]
   (thm "zpower_number_of_odd"))]
 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/HOL/Real/ferrante_rackoff.ML
--- a/src/HOL/Real/ferrante_rackoff.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Real/ferrante_rackoff.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -42,7 +42,7 @@
 val powerarith =
   map thm ["nat_number_of", "zpower_number_of_even",
   "zpower_Pls", "zpower_Min"]
-  @ [Tactic.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
+  @ [MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
     (thm "zpower_number_of_odd")]
 
 val comp_arith = binarith @ intarith @ intarithrel @ natarith 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -56,7 +56,7 @@
 val powerarith =
     (map thm ["nat_number_of", "zpower_number_of_even",
               "zpower_Pls", "zpower_Min"]) @
-    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
+    [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
                            thm "one_eq_Numeral1_nring"]
   (thm "zpower_number_of_odd"))]
 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -375,7 +375,7 @@
   in map mk_dist (sym_product cos) end;
 
 local
-  val bool_eq_implies = thm "iffD1";
+  val bool_eq_implies = iffD1;
   val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
   val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
   val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
@@ -387,7 +387,7 @@
     val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
     val inject = (#inject o DatatypePackage.the_datatype thy) dtco
       |> map (fn thm => bool_eq_implies OF [thm] )
-      |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
+      |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]);
     val ctxt = ProofContext.init thy;
     val simpset = Simplifier.context ctxt
       (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -1428,7 +1428,7 @@
       let
         val SOME { Abs_induct = abs_induct,
           Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
-        val rewrite_rule = Tactic.rewrite_rule [rec_UNIV_I, rec_True_simp];
+        val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
       in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
   in
     thy
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -96,7 +96,7 @@
     val tac = Tactic.rtac UNIV_witness 1;
     fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
       Rep_name = c_rep, Abs_inject = inject,
-      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = 
+      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
         let
           val exists_thm =
             UNIV_I
@@ -146,16 +146,16 @@
   in (vs, [(constr, [typ])]) end;
 
 local
-  val bool_eq_implies = thm "iffD1";
+  val bool_eq_implies = iffD1;
   val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
 in fun get_cert thy tyco =
-  Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
+  MetaSimplifier.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
 end; (*local*)
 
 
 (* hook for projection function code *)
 
-fun add_project (_ , { proj_def, ...} : info) =
+fun add_project (_ , {proj_def, ...} : info) =
   CodegenData.add_func proj_def;
 
 val setup =
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Provers/eqsubst.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -415,7 +415,7 @@
       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
       val preelimrule =
           (RWInst.rw m rule pth)
-            |> (Seq.hd o Tactic.prune_params_tac)
+            |> (Seq.hd o prune_params_tac)
             |> Thm.permute_prems 0 ~1 (* put old asm first *)
             |> IsaND.unfix_frees cfvs (* unfix any global params *)
             |> RWInst.beta_eta_contract; (* normal form *)
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Provers/induct_method.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -160,7 +160,7 @@
   MetaSimplifier.rewrite_term thy Data.atomize []
   #> ObjectLogic.drop_judgment thy;
 
-val atomize_cterm = Tactic.rewrite true Data.atomize;
+val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
 
 val atomize_tac = Goal.rewrite_goal_tac Data.atomize;
 
@@ -312,7 +312,7 @@
 
 fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
   (Drule.goals_conv (Library.equal i)
-    (Drule.forall_conv p (Tactic.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
+    (Drule.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
 
 in
 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -161,11 +161,11 @@
 
 fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
 
-val unfold       = meta Tactic.rewrite_rule;
-val unfold_goals = meta Tactic.rewrite_goals_rule;
-val unfold_tac   = meta Tactic.rewrite_goals_tac;
-val fold         = meta Tactic.fold_rule;
-val fold_tac     = meta Tactic.fold_goals_tac;
+val unfold       = meta MetaSimplifier.rewrite_rule;
+val unfold_goals = meta MetaSimplifier.rewrite_goals_rule;
+val unfold_tac   = meta MetaSimplifier.rewrite_goals_tac;
+val fold         = meta MetaSimplifier.fold_rule;
+val fold_tac     = meta MetaSimplifier.fold_goals_tac;
 
 
 (* derived defs -- potentially within the object-logic *)
@@ -186,7 +186,7 @@
         Goal.prove ctxt' frees [] prop (K (ALLGOALS
           (meta_rewrite_tac ctxt' THEN'
             Goal.rewrite_goal_tac [def] THEN'
-            Tactic.resolve_tac [Drule.reflexive_thm])))
+            resolve_tac [Drule.reflexive_thm])))
         handle ERROR msg => cat_error msg "Failed to prove definitional specification."
       end;
   in (((c, T), rhs), prove) end;
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -1648,17 +1648,17 @@
     val cert = Thm.cterm_of defs_thy;
 
     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
-      Tactic.rewrite_goals_tac [pred_def] THEN
+      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
       Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq,
-        Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
+        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_precise [length ts] |> hd;
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness defs_ctxt t
-       (Tactic.rewrite_goals_tac defs THEN
+       (MetaSimplifier.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -148,12 +148,12 @@
 fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule
   (Drule.goals_conv (Library.equal i)
     (Drule.forall_conv ~1
-      (Drule.goals_conv (K true) (Tactic.rewrite true rews)))));
+      (Drule.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
 
 fun atomize_term thy =
   drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
 
-fun atomize_cterm ct = Tactic.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
+fun atomize_cterm ct = MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
 fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
 
 fun atomize_tac i st =
@@ -174,7 +174,7 @@
 fun rulify_tac i st = Goal.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
 
 fun gen_rulify full thm =
-  Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
+  MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
 
 val rulify = gen_rulify true;
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -189,14 +189,14 @@
 
 fun unfold_prems n defs th =
   if null defs then th
-  else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs)) th;
+  else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
 
 fun unfold_prems_concls defs th =
   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   else
     Drule.fconv_rule
       (Drule.concl_conv ~1 (Conjunction.conv ~1
-        (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
+        (K (Drule.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
 
 in
 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -92,7 +92,7 @@
     val thy_ctxt = ProofContext.init thy;
     val ct = Thm.cterm_of thy t;
     val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
-  in (Thm.term_of ct', Tactic.rewrite true defs ct) end;
+  in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end;
 
 fun add_def (name, prop) =
   Theory.add_defs_i false false [(name, prop)] #>
@@ -171,8 +171,8 @@
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
     val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
-    val concl_conv = Tactic.rewrite true defs (Thm.cprop_of th);
-    val assms = map (Tactic.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
+    val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
+    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
     val nprems = Thm.nprems_of th' - Thm.nprems_of th;
 
     (*export fixes*)
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/ROOT.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -55,8 +55,8 @@
 use "variable.ML";
 use "tctical.ML";
 use "search.ML";
+use "tactic.ML";
 use "meta_simplifier.ML";
-use "tactic.ML";
 use "conjunction.ML";
 use "assumption.ML";
 use "goal.ML";
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -185,7 +185,7 @@
     val class = loc (*FIXME*);
     val thms = (#defs o fst o the_class_data thy) class;
   in
-    Tactic.rewrite_rule thms
+    MetaSimplifier.rewrite_rule thms
   end;
 
 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Tools/codegen_data.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -524,7 +524,7 @@
 
 fun rewrite_func rewrites thm =
   let
-    val rewrite = Tactic.rewrite false rewrites;
+    val rewrite = MetaSimplifier.rewrite false rewrites;
     val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm;
     val Const ("==", _) = Thm.term_of ct_eq;
     val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
@@ -715,7 +715,7 @@
   ((fn [args, rhs] => rhs :: (snd o Drule.strip_comb) args) o snd o Drule.strip_comb o Thm.cprop_of))
   (fn rews => map (rewrite_func rews));
 val apply_inline_proc_cterm = gen_apply_inline_proc single
-  (Tactic.rewrite false);
+  (MetaSimplifier.rewrite false);
 
 fun apply_preproc thy f [] = []
   | apply_preproc thy f (thms as (thm :: _)) =
@@ -746,8 +746,10 @@
 fun preprocess_cterm thy ct =
   ct
   |> Thm.reflexive
-  |> fold (rhs_conv o Tactic.rewrite false o single) ((#inlines o the_preproc o get_exec) thy)
-  |> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f)) ((#inline_procs o the_preproc o get_exec) thy)
+  |> fold (rhs_conv o MetaSimplifier.rewrite false o single)
+    ((#inlines o the_preproc o get_exec) thy)
+  |> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f))
+    ((#inline_procs o the_preproc o get_exec) thy)
 
 end; (*local*)
 
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/Tools/nbe.ML
--- a/src/Pure/Tools/nbe.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/Tools/nbe.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -78,7 +78,7 @@
   let
     val ctxt = ProofContext.init thy;
     val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (NBE_Rewrite.get thy)
-  in Tactic.rewrite false posts end
+  in MetaSimplifier.rewrite false posts end
 
 
 (* code store *)
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -72,6 +72,16 @@
   val addSSolver: simpset * solver -> simpset
   val setSolver: simpset * solver -> simpset
   val addSolver: simpset * solver -> simpset
+
+  val rewrite_rule: thm list -> thm -> thm
+  val rewrite_goals_rule: thm list -> thm -> thm
+  val rewrite_goals_tac: thm list -> tactic
+  val rewrite_tac: thm list -> tactic
+  val rewtac: thm -> tactic
+  val prune_params_tac: tactic
+  val fold_rule: thm list -> thm -> thm
+  val fold_tac: thm list -> tactic
+  val fold_goals_tac: thm list -> tactic
 end;
 
 signature META_SIMPLIFIER =
@@ -94,16 +104,15 @@
   val set_solvers: solver list -> simpset -> simpset
   val rewrite_cterm: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> cterm -> thm
-  val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
-  val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
   val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
   val rewrite_thm: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> thm -> thm
-  val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_goal_rule: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
   val norm_hhf: thm -> thm
   val norm_hhf_protect: thm -> thm
+  val rewrite: bool -> thm list -> cterm -> thm
+  val simplify: bool -> thm list -> thm -> thm
 end;
 
 structure MetaSimplifier: META_SIMPLIFIER =
@@ -1189,18 +1198,23 @@
   in dec simp_depth; res end
   handle exn => (dec simp_depth; raise exn);  (* FIXME avoid handling of generic exceptions *)
 
+val simple_prover =
+  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
+
 (*Rewrite a cterm*)
-fun rewrite_aux _ _ [] ct = Thm.reflexive ct
-  | rewrite_aux prover full thms ct =
-      rewrite_cterm (full, false, false) prover
-      (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
+fun rewrite _ [] ct = Thm.reflexive ct
+  | rewrite full thms ct =
+      rewrite_cterm (full, false, false) simple_prover
+        (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 
 (*Rewrite a theorem*)
-fun simplify_aux _ _ [] th = th
-  | simplify_aux prover full thms th =
-      Drule.fconv_rule (rewrite_cterm (full, false, false) prover
+fun simplify _ [] th = th
+  | simplify full thms th =
+      Drule.fconv_rule (rewrite_cterm (full, false, false) simple_prover
         (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th;
 
+val rewrite_rule = simplify true;
+
 (*simple term rewriting -- no proof*)
 fun rewrite_term thy rules procs =
   Pattern.rewrite_term thy (map decomp_simp' rules) procs;
@@ -1208,8 +1222,8 @@
 fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
 
 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
-fun rewrite_goals_rule_aux prover thms th =
-  Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) prover
+fun rewrite_goals_rule thms th =
+  Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover
     (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 
 (*Rewrite the subgoal of a proof state (represented by a theorem)*)
@@ -1219,6 +1233,44 @@
   else raise THM("rewrite_goal_rule",i,[thm]);
 
 
+(** meta-rewriting tactics **)
+
+(*Rewrite throughout proof state. *)
+fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
+
+(*Rewrite subgoals only, not main goal. *)
+fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
+fun rewtac def = rewrite_goals_tac [def];
+
+(*Prunes all redundant parameters from the proof state by rewriting.
+  DOES NOT rewrite main goal, where quantification over an unused bound
+    variable is sometimes done to avoid the need for cut_facts_tac.*)
+val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
+
+
+(* for folding definitions, handling critical pairs *)
+
+(*The depth of nesting in a term*)
+fun term_depth (Abs(a,T,t)) = 1 + term_depth t
+  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
+  | term_depth _ = 0;
+
+val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
+
+(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
+  Returns longest lhs first to avoid folding its subexpressions.*)
+fun sort_lhs_depths defs =
+  let val keylist = AList.make (term_depth o lhs_of_thm) defs
+      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
+  in map (AList.find (op =) keylist) keys end;
+
+val rev_defs = sort_lhs_depths o map symmetric;
+
+fun fold_rule defs = fold rewrite_rule (rev_defs defs);
+fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
+fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
+
+
 (* HHF normal form: !! before ==>, outermost !! generalized *)
 
 local
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/simplifier.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -80,6 +80,9 @@
 structure Simplifier: SIMPLIFIER =
 struct
 
+open MetaSimplifier;
+
+
 (** simpset data **)
 
 (* global simpsets *)
@@ -348,9 +351,6 @@
     thy
   end);
 
-
-open MetaSimplifier;
-
 end;
 
 structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/tactic.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -47,9 +47,6 @@
   val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
   val filt_resolve_tac  : thm list -> int -> int -> tactic
   val flexflex_tac      : tactic
-  val fold_goals_tac    : thm list -> tactic
-  val fold_rule         : thm list -> thm -> thm
-  val fold_tac          : thm list -> tactic
   val forward_tac       : thm list -> int -> tactic
   val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
   val ftac              : thm -> int ->tactic
@@ -69,18 +66,12 @@
   val net_biresolve_tac : (bool*thm) list -> int -> tactic
   val net_match_tac     : thm list -> int -> tactic
   val net_resolve_tac   : thm list -> int -> tactic
-  val prune_params_tac  : tactic
   val rename_params_tac : string list -> int -> tactic
   val rename_tac        : string -> int -> tactic
   val rename_last_tac   : string -> string list -> int -> tactic
   val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
   val resolve_tac       : thm list -> int -> tactic
   val res_inst_tac      : (string*string)list -> thm -> int -> tactic
-  val rewrite_goals_rule: thm list -> thm -> thm
-  val rewrite_rule      : thm list -> thm -> thm
-  val rewrite_goals_tac : thm list -> tactic
-  val rewrite_tac       : thm list -> tactic
-  val rewtac            : thm -> tactic
   val rotate_tac        : int -> int -> tactic
   val rtac              : thm -> int -> tactic
   val rule_by_tactic    : tactic -> thm -> thm
@@ -103,8 +94,6 @@
   val untaglist: (int * 'a) list -> 'a list
   val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
   val orderlist: (int * 'a) list -> 'a list
-  val rewrite: bool -> thm list -> cterm -> thm
-  val simplify: bool -> thm list -> thm -> thm
   val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
                           int -> tactic
   val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
@@ -512,47 +501,6 @@
 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
 
 
-(*** Meta-Rewriting Tactics ***)
-
-val simple_prover =
-  SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
-
-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 throughout proof state. *)
-fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
-
-(*Rewrite subgoals only, not main goal. *)
-fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
-fun rewtac def = rewrite_goals_tac [def];
-
-
-(*** for folding definitions, handling critical pairs ***)
-
-(*The depth of nesting in a term*)
-fun term_depth (Abs(a,T,t)) = 1 + term_depth t
-  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
-  | term_depth _ = 0;
-
-val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
-
-(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
-  Returns longest lhs first to avoid folding its subexpressions.*)
-fun sort_lhs_depths defs =
-  let val keylist = AList.make (term_depth o lhs_of_thm) defs
-      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
-  in map (AList.find (op =) keylist) keys end;
-
-val rev_defs = sort_lhs_depths o map symmetric;
-
-fun fold_rule defs = fold rewrite_rule (rev_defs defs);
-fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
-fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
-
-
 (*** Renaming of parameters in a subgoal
      Names may contain letters, digits or primes and must be
      separated by blanks ***)
@@ -582,11 +530,6 @@
       else all_tac
   end;
 
-(*Prunes all redundant parameters from the proof state by rewriting.
-  DOES NOT rewrite main goal, where quantification over an unused bound
-    variable is sometimes done to avoid the need for cut_facts_tac.*)
-val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
-
 (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   right to left if n is positive, and from left to right if n is negative.*)
 fun rotate_tac 0 i = all_tac