Made simplification procedures simpset-aware.
authorskalberg
Wed Jun 30 00:42:59 2004 +0200 (2004-06-30)
changeset 1501135be762f58f9
parent 15010 72fbe711e414
child 15012 28fa57b57209
Made simplification procedures simpset-aware.
NEWS
TFL/rules.ML
src/Pure/meta_simplifier.ML
src/Pure/tactic.ML
     1.1 --- a/NEWS	Tue Jun 29 11:18:34 2004 +0200
     1.2 +++ b/NEWS	Wed Jun 30 00:42:59 2004 +0200
     1.3 @@ -6,6 +6,11 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Pure: Simplification procedures can now take the current simpset as
     1.8 +  an additional argument; This is useful for calling the simplifier
     1.9 +  recursively.  See the functions MetaSimplifier.full_{mk_simproc,
    1.10 +  simproc,simproc_i}.
    1.11 +
    1.12  * Pure: considerably improved version of 'constdefs' command.  Now
    1.13    performs automatic type-inference of declared constants; additional
    1.14    support for local structure declarations (cf. locales and HOL
     2.1 --- a/TFL/rules.ML	Tue Jun 29 11:18:34 2004 +0200
     2.2 +++ b/TFL/rules.ML	Wed Jun 30 00:42:59 2004 +0200
     2.3 @@ -433,7 +433,7 @@
     2.4  local fun rew_conv mss = MetaSimplifier.rewrite_cterm (true,false,false) (K(K None)) mss
     2.5  in
     2.6  fun simpl_conv ss thl ctm =
     2.7 - rew_conv (MetaSimplifier.mss_of (#simps (MetaSimplifier.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
     2.8 + rew_conv (MetaSimplifier.ss_of (#simps (MetaSimplifier.dest_mss (#mss (rep_ss ss))) @ thl)) ctm
     2.9   RS meta_eq_to_obj_eq
    2.10  end;
    2.11  
    2.12 @@ -688,7 +688,7 @@
    2.13                       val eq = Logic.strip_imp_concl imp
    2.14                       val lhs = tych(get_lhs eq)
    2.15                       val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants)
    2.16 -                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' lhs
    2.17 +                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) (MetaSimplifier.from_mss mss') lhs
    2.18                         handle U.ERR _ => Thm.reflexive lhs
    2.19                       val dummy = print_thms "proven:" [lhs_eq_lhs1]
    2.20                       val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
    2.21 @@ -710,7 +710,7 @@
    2.22                    val QeqQ1 = pbeta_reduce (tych Q)
    2.23                    val Q1 = #2(D.dest_eq(cconcl QeqQ1))
    2.24                    val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
    2.25 -                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
    2.26 +                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') (MetaSimplifier.from_mss mss') Q1
    2.27                                  handle U.ERR _ => Thm.reflexive Q1
    2.28                    val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
    2.29                    val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
    2.30 @@ -736,7 +736,7 @@
    2.31                       val ants1 = map tych ants
    2.32                       val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
    2.33                       val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
    2.34 -                        (false,true,false) (prover used') mss' (tych Q)
    2.35 +                        (false,true,false) (prover used') (MetaSimplifier.from_mss mss') (tych Q)
    2.36                        handle U.ERR _ => Thm.reflexive (tych Q)
    2.37                       val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
    2.38                       val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
    2.39 @@ -806,7 +806,7 @@
    2.40      val ctm = cprop_of th
    2.41      val names = add_term_names (term_of ctm, [])
    2.42      val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
    2.43 -      (prover names) (MetaSimplifier.add_congs(MetaSimplifier.mss_of [cut_lemma'], congs)) ctm
    2.44 +      (prover names) (MetaSimplifier.addeqcongs(MetaSimplifier.ss_of [cut_lemma'], congs)) ctm
    2.45      val th2 = equal_elim th1 th
    2.46   in
    2.47   (th2, filter (not o restricted) (!tc_list))
     3.1 --- a/src/Pure/meta_simplifier.ML	Tue Jun 29 11:18:34 2004 +0200
     3.2 +++ b/src/Pure/meta_simplifier.ML	Wed Jun 30 00:42:59 2004 +0200
     3.3 @@ -20,12 +20,14 @@
     3.4  signature AUX_SIMPLIFIER =
     3.5  sig
     3.6    type meta_simpset
     3.7 +  type simpset
     3.8    type simproc
     3.9 +  val full_mk_simproc: string -> cterm list
    3.10 +    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
    3.11    val mk_simproc: string -> cterm list
    3.12      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    3.13    type solver
    3.14    val mk_solver: string -> (thm list -> int -> tactic) -> solver
    3.15 -  type simpset
    3.16    val empty_ss: simpset
    3.17    val rep_ss: simpset ->
    3.18     {mss: meta_simpset,
    3.19 @@ -33,7 +35,9 @@
    3.20      subgoal_tac: simpset -> int -> tactic,
    3.21      loop_tacs: (string * (int -> tactic)) list,
    3.22      unsafe_solvers: solver list,
    3.23 -    solvers: solver list};
    3.24 +    solvers: solver list}
    3.25 +  val from_mss: meta_simpset -> simpset
    3.26 +  val ss_of            : thm list -> simpset
    3.27    val print_ss: simpset -> unit
    3.28    val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    3.29    val setloop:      simpset *             (int -> tactic) -> simpset
    3.30 @@ -63,6 +67,10 @@
    3.31      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    3.32    val simproc_i: Sign.sg -> string -> term list
    3.33      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    3.34 +  val full_simproc: Sign.sg -> string -> string list
    3.35 +    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
    3.36 +  val full_simproc_i: Sign.sg -> string -> term list
    3.37 +    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
    3.38    val clear_ss  : simpset -> simpset
    3.39    val simp_thm  : bool * bool * bool -> simpset -> thm -> thm
    3.40    val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm
    3.41 @@ -85,10 +93,10 @@
    3.42    val add_congs         : meta_simpset * thm list -> meta_simpset
    3.43    val del_congs         : meta_simpset * thm list -> meta_simpset
    3.44    val add_simprocs      : meta_simpset *
    3.45 -    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    3.46 +    (string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp) list
    3.47        -> meta_simpset
    3.48    val del_simprocs      : meta_simpset *
    3.49 -    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    3.50 +    (string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp) list
    3.51        -> meta_simpset
    3.52    val add_prems         : meta_simpset * thm list -> meta_simpset
    3.53    val prems_of_mss      : meta_simpset -> thm list
    3.54 @@ -100,19 +108,19 @@
    3.55    val get_mk_eq_True    : meta_simpset -> thm -> thm option
    3.56    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    3.57    val rewrite_cterm: bool * bool * bool ->
    3.58 -    (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
    3.59 +    (meta_simpset -> thm -> thm option) -> simpset -> cterm -> thm
    3.60    val rewrite_aux       : (meta_simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
    3.61    val simplify_aux      : (meta_simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
    3.62    val rewrite_thm       : bool * bool * bool
    3.63                            -> (meta_simpset -> thm -> thm option)
    3.64 -                          -> meta_simpset -> thm -> thm
    3.65 +                          -> simpset -> thm -> thm
    3.66    val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    3.67    val rewrite_goal_rule : bool* bool * bool
    3.68                            -> (meta_simpset -> thm -> thm option)
    3.69 -                          -> meta_simpset -> int -> thm -> thm
    3.70 +                          -> simpset -> int -> thm -> thm
    3.71    val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
    3.72    val asm_rewrite_goal_tac: bool*bool*bool ->
    3.73 -    (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    3.74 +    (meta_simpset -> tactic) -> simpset -> int -> tactic
    3.75  
    3.76  end;
    3.77  
    3.78 @@ -181,8 +189,6 @@
    3.79         in which case there is nothing better to do.
    3.80  *)
    3.81  type cong = {thm: thm, lhs: cterm};
    3.82 -type meta_simproc =
    3.83 - {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
    3.84  
    3.85  fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
    3.86    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
    3.87 @@ -193,11 +199,6 @@
    3.88  fun eq_prem (thm1, thm2) =
    3.89    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
    3.90  
    3.91 -fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
    3.92 -
    3.93 -fun mk_simproc (name, proc, lhs, id) =
    3.94 -  {name = name, proc = proc, lhs = lhs, id = id};
    3.95 -
    3.96  
    3.97  (* datatype mss *)
    3.98  
    3.99 @@ -219,6 +220,8 @@
   3.100      depth: depth of conditional rewriting;
   3.101  *)
   3.102  
   3.103 +datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   3.104 +
   3.105  datatype meta_simpset =
   3.106    Mss of {
   3.107      rules: rrule Net.net,
   3.108 @@ -230,7 +233,17 @@
   3.109                mk_sym: thm -> thm option,
   3.110                mk_eq_True: thm -> thm option},
   3.111      termless: term * term -> bool,
   3.112 -    depth: int};
   3.113 +    depth: int}
   3.114 +and simpset =
   3.115 +  Simpset of {
   3.116 +    mss: meta_simpset,
   3.117 +    mk_cong: thm -> thm,
   3.118 +    subgoal_tac: simpset -> int -> tactic,
   3.119 +    loop_tacs: (string * (int -> tactic)) list,
   3.120 +    unsafe_solvers: solver list,
   3.121 +    solvers: solver list}
   3.122 +withtype meta_simproc =
   3.123 + {name: string, proc: simpset -> Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
   3.124  
   3.125  fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth) =
   3.126    Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
   3.127 @@ -257,6 +270,14 @@
   3.128            )
   3.129    end;
   3.130  
   3.131 +datatype simproc =
   3.132 +  Simproc of string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp
   3.133 +
   3.134 +fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
   3.135 +
   3.136 +fun mk_simproc (name, proc, lhs, id) =
   3.137 +  {name = name, proc = proc, lhs = lhs, id = id};
   3.138 +
   3.139  
   3.140  (** simpset operations **)
   3.141  
   3.142 @@ -591,11 +612,15 @@
   3.143  
   3.144  (* datatype simproc *)
   3.145  
   3.146 -datatype simproc =
   3.147 -  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
   3.148 +fun full_mk_simproc name lhss proc =
   3.149 +  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   3.150 +
   3.151 +fun full_simproc sg name ss =
   3.152 +  full_mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
   3.153 +fun full_simproc_i sg name = full_mk_simproc name o map (Thm.cterm_of sg);
   3.154  
   3.155  fun mk_simproc name lhss proc =
   3.156 -  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   3.157 +  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, K proc, stamp ());
   3.158  
   3.159  fun simproc sg name ss =
   3.160    mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
   3.161 @@ -607,8 +632,6 @@
   3.162  
   3.163  (** solvers **)
   3.164  
   3.165 -datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   3.166 -
   3.167  fun mk_solver name solver = Solver (name, solver, stamp());
   3.168  fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
   3.169  
   3.170 @@ -624,22 +647,13 @@
   3.171  
   3.172  (* type simpset *)
   3.173  
   3.174 -datatype simpset =
   3.175 -  Simpset of {
   3.176 -    mss: meta_simpset,
   3.177 -    mk_cong: thm -> thm,
   3.178 -    subgoal_tac: simpset -> int -> tactic,
   3.179 -    loop_tacs: (string * (int -> tactic)) list,
   3.180 -    unsafe_solvers: solver list,
   3.181 -    solvers: solver list};
   3.182 -
   3.183  fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
   3.184    Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
   3.185      loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
   3.186  
   3.187 -val empty_ss =
   3.188 -  let val mss = set_mk_sym (empty_mss, Some o symmetric_fun)
   3.189 -  in make_ss mss I (K (K no_tac)) [] [] [] end;
   3.190 +fun from_mss mss = make_ss mss I (K (K no_tac)) [] [] [];
   3.191 +
   3.192 +val empty_ss = from_mss (set_mk_sym (empty_mss, Some o symmetric_fun));
   3.193  
   3.194  fun rep_ss (Simpset args) = args;
   3.195  fun prems_of_ss (Simpset {mss, ...}) = prems_of_mss mss;
   3.196 @@ -850,7 +864,7 @@
   3.197  *)
   3.198  
   3.199  fun rewritec (prover, signt, maxt)
   3.200 -             (mss as Mss{rules, procs, termless, prems, congs, depth,...}) t =
   3.201 +             (ss as Simpset{mss=mss as Mss{rules, procs, termless, prems, congs, depth,...},...}) t =
   3.202    let
   3.203      val eta_thm = Thm.eta_conversion t;
   3.204      val eta_t' = rhs_of eta_thm;
   3.205 @@ -917,7 +931,7 @@
   3.206            if Pattern.matches tsigt (term_of lhs, term_of t) then
   3.207              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   3.208               case transform_failure (curry SIMPROC_FAIL name)
   3.209 -                 (fn () => proc signt prems eta_t) () of
   3.210 +                 (fn () => proc ss signt prems eta_t) () of
   3.211                 None => (debug false "FAILED"; proc_rews ps)
   3.212               | Some raw_thm =>
   3.213                   (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   3.214 @@ -969,20 +983,24 @@
   3.215  fun transitive2 thm = transitive1 (Some thm);
   3.216  fun transitive3 thm = transitive1 thm o Some;
   3.217  
   3.218 -fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   3.219 +fun replace_mss (Simpset{mss=_,mk_cong,subgoal_tac,loop_tacs,unsafe_solvers,solvers}) mss_new =
   3.220 +    Simpset{mss=mss_new,mk_cong=mk_cong,subgoal_tac=subgoal_tac,loop_tacs=loop_tacs,
   3.221 +	    unsafe_solvers=unsafe_solvers,solvers=solvers};
   3.222 +
   3.223 +fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) (ss as Simpset{mss,...}) =
   3.224    let
   3.225      fun botc skel mss t =
   3.226            if is_Var skel then None
   3.227            else
   3.228            (case subc skel mss t of
   3.229               some as Some thm1 =>
   3.230 -               (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   3.231 +               (case rewritec (prover, sign, maxidx) (replace_mss ss mss) (rhs_of thm1) of
   3.232                    Some (thm2, skel2) =>
   3.233                      transitive2 (transitive thm1 thm2)
   3.234                        (botc skel2 mss (rhs_of thm2))
   3.235                  | None => some)
   3.236             | None =>
   3.237 -               (case rewritec (prover, sign, maxidx) mss t of
   3.238 +               (case rewritec (prover, sign, maxidx) (replace_mss ss mss) t of
   3.239                    Some (thm2, skel2) => transitive2 thm2
   3.240                      (botc skel2 mss (rhs_of thm2))
   3.241                  | None => None))
   3.242 @@ -1093,7 +1111,7 @@
   3.243              val concl' =
   3.244                Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl);
   3.245              val dprem = apsome (curry (disch false) prem)
   3.246 -          in case rewritec (prover, sign, maxidx) mss' concl' of
   3.247 +          in case rewritec (prover, sign, maxidx) (replace_mss ss mss') concl' of
   3.248                None => rebuild prems concl' rrss asms mss (dprem eq)
   3.249              | Some (eq', _) => transitive2 (foldl (disch false o swap)
   3.250                    (the (transitive3 (dprem eq) eq'), prems))
   3.251 @@ -1157,7 +1175,7 @@
   3.252             end)
   3.253         end
   3.254  
   3.255 - in try_botc end;
   3.256 + in try_botc mss end;
   3.257  
   3.258  
   3.259  (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
   3.260 @@ -1172,25 +1190,27 @@
   3.261      prover: how to solve premises in conditional rewrites and congruences
   3.262  *)
   3.263  
   3.264 -fun rewrite_cterm mode prover mss ct =
   3.265 +fun rewrite_cterm mode prover (ss as Simpset{mss,...}) ct =
   3.266    let val {sign, t, maxidx, ...} = rep_cterm ct
   3.267        val Mss{depth, ...} = mss
   3.268    in trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
   3.269       simp_depth := depth;
   3.270 -     bottomc (mode, prover, sign, maxidx) mss ct
   3.271 +     bottomc (mode, prover, sign, maxidx) ss ct
   3.272    end
   3.273    handle THM (s, _, thms) =>
   3.274      error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   3.275        Pretty.string_of (Display.pretty_thms thms));
   3.276  
   3.277 +val ss_of = from_mss o mss_of
   3.278 +
   3.279  (*Rewrite a cterm*)
   3.280  fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
   3.281 -  | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (mss_of thms);
   3.282 +  | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (ss_of thms);
   3.283  
   3.284  (*Rewrite a theorem*)
   3.285  fun simplify_aux _ _ [] = (fn th => th)
   3.286    | simplify_aux prover full thms =
   3.287 -      Drule.fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
   3.288 +      Drule.fconv_rule (rewrite_cterm (full, false, false) prover (ss_of thms));
   3.289  
   3.290  fun rewrite_thm mode prover mss = Drule.fconv_rule (rewrite_cterm mode prover mss);
   3.291  
   3.292 @@ -1198,12 +1218,12 @@
   3.293  fun rewrite_goals_rule_aux _ []   th = th
   3.294    | rewrite_goals_rule_aux prover thms th =
   3.295        Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, false) prover
   3.296 -        (mss_of thms))) th;
   3.297 +        (ss_of thms))) th;
   3.298  
   3.299  (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   3.300 -fun rewrite_goal_rule mode prover mss i thm =
   3.301 +fun rewrite_goal_rule mode prover ss i thm =
   3.302    if 0 < i  andalso  i <= nprems_of thm
   3.303 -  then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   3.304 +  then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
   3.305    else raise THM("rewrite_goal_rule",i,[thm]);
   3.306  
   3.307  
   3.308 @@ -1229,25 +1249,25 @@
   3.309  
   3.310  (*note: may instantiate unknowns that appear also in other subgoals*)
   3.311  fun generic_simp_tac safe mode =
   3.312 -  fn (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   3.313 +  fn (ss as Simpset {mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   3.314      let
   3.315        val solvs = app_sols (if safe then solvers else unsafe_solvers);
   3.316        fun simp_loop_tac i =
   3.317          asm_rewrite_goal_tac mode
   3.318            (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
   3.319 -          mss i
   3.320 -        THEN (solvs (prems_of_mss mss) i ORELSE
   3.321 +          ss i
   3.322 +        THEN (solvs (prems_of_ss ss) i ORELSE
   3.323                TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   3.324      in simp_loop_tac end;
   3.325  
   3.326  (** simplification rules and conversions **)
   3.327  
   3.328  fun simp rew mode
   3.329 -     (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   3.330 +     (ss as Simpset {mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   3.331    let
   3.332      val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
   3.333      fun prover m th = apsome fst (Seq.pull (tacf m th));
   3.334 -  in rew mode prover mss thm end;
   3.335 +  in rew mode prover ss thm end;
   3.336  
   3.337  val simp_thm = simp rewrite_thm;
   3.338  val simp_cterm = simp rewrite_cterm;
     4.1 --- a/src/Pure/tactic.ML	Tue Jun 29 11:18:34 2004 +0200
     4.2 +++ b/src/Pure/tactic.ML	Wed Jun 30 00:42:59 2004 +0200
     4.3 @@ -498,7 +498,7 @@
     4.4  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
     4.5  
     4.6  fun rewrite_goal_tac rews =
     4.7 -  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
     4.8 +  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.ss_of rews);
     4.9  
    4.10  (*Rewrite throughout proof state. *)
    4.11  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);