1.1 --- a/src/Pure/goal.ML	Tue Jul 03 17:17:09 2007 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Jul 03 17:17:11 2007 +0200
     1.3 @@ -32,8 +32,6 @@
     1.4    val conjunction_tac: int -> tactic
     1.5    val precise_conjunction_tac: int -> int -> tactic
     1.6    val recover_conjunction_tac: tactic
     1.7 -  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
     1.8 -  val rewrite_goal_tac: thm list -> int -> tactic
     1.9    val norm_hhf_tac: int -> tactic
    1.10    val compose_hhf: thm -> int -> thm -> thm Seq.seq
    1.11    val compose_hhf_tac: thm -> int -> tactic
    1.12 @@ -209,27 +207,13 @@
    1.13      THEN recover_conjunction_tac);
    1.14  
    1.15  
    1.16 -(* rewriting *)
    1.17 -
    1.18 -(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    1.19 -fun asm_rewrite_goal_tac mode prover_tac ss =
    1.20 -  SELECT_GOAL
    1.21 -    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
    1.22 -
    1.23 -fun rewrite_goal_tac rews =
    1.24 -  let val ss = MetaSimplifier.empty_ss addsimps rews in
    1.25 -    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.26 -      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
    1.27 -  end;
    1.28 -
    1.29 -
    1.30  (* hhf normal form *)
    1.31  
    1.32  val norm_hhf_tac =
    1.33    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.34    THEN' SUBGOAL (fn (t, i) =>
    1.35      if Drule.is_norm_hhf t then all_tac
    1.36 -    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.37 +    else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.38  
    1.39  fun compose_hhf tha i thb =
    1.40    Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;

     2.1 --- a/src/Pure/meta_simplifier.ML	Tue Jul 03 17:17:09 2007 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Tue Jul 03 17:17:11 2007 +0200
     2.3 @@ -81,6 +81,7 @@
     2.4    val rewrite_goals_rule: thm list -> thm -> thm
     2.5    val rewrite_goals_tac: thm list -> tactic
     2.6    val rewrite_tac: thm list -> tactic
     2.7 +  val rewrite_goal_tac: thm list -> int -> tactic
     2.8    val rewtac: thm -> tactic
     2.9    val prune_params_tac: tactic
    2.10    val fold_rule: thm list -> thm -> thm
    2.11 @@ -113,6 +114,8 @@
    2.12      (simpset -> thm -> thm option) -> simpset -> thm -> thm
    2.13    val rewrite_goal_rule: bool * bool * bool ->
    2.14      (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
    2.15 +  val asm_rewrite_goal_tac: bool * bool * bool ->
    2.16 +    (simpset -> tactic) -> simpset -> int -> tactic
    2.17    val norm_hhf: thm -> thm
    2.18    val norm_hhf_protect: thm -> thm
    2.19    val rewrite: bool -> thm list -> cterm -> thm
    2.20 @@ -1266,27 +1269,37 @@
    2.21  
    2.22  fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
    2.23  
    2.24 -(*Rewrite the subgoals of a proof state (represented by a theorem) *)
    2.25 +(*Rewrite the subgoals of a proof state (represented by a theorem)*)
    2.26  fun rewrite_goals_rule thms th =
    2.27 -  Conv.fconv_rule (Conv.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover
    2.28 -    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
    2.29 +  Conv.fconv_rule (Conv.prems_conv ~1 (K (rewrite_cterm (true, true, true) simple_prover
    2.30 +    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)))) th;
    2.31  
    2.32  (*Rewrite the subgoal of a proof state (represented by a theorem)*)
    2.33  fun rewrite_goal_rule mode prover ss i thm =
    2.34 -  if 0 < i  andalso  i <= nprems_of thm
    2.35 -  then Conv.fconv_rule (Conv.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
    2.36 -  else raise THM("rewrite_goal_rule", i, [thm]);
    2.37 +  if 0 < i andalso i <= Thm.nprems_of thm
    2.38 +  then Conv.goal_conv_rule (rewrite_cterm mode prover ss) i thm
    2.39 +  else raise THM ("rewrite_goal_rule", i, [thm]);
    2.40  
    2.41  
    2.42  (** meta-rewriting tactics **)
    2.43  
    2.44  (*Rewrite throughout proof state. *)
    2.45 -fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
    2.46 +fun rewrite_tac defs = PRIMITIVE (rewrite_rule defs);
    2.47  
    2.48  (*Rewrite subgoals only, not main goal. *)
    2.49  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    2.50  fun rewtac def = rewrite_goals_tac [def];
    2.51  
    2.52 +(*Rewrite subgoal i only.*)
    2.53 +fun asm_rewrite_goal_tac mode prover_tac ss i =
    2.54 +  PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) ss i);
    2.55 +
    2.56 +fun rewrite_goal_tac rews =
    2.57 +  let val ss = empty_ss addsimps rews in
    2.58 +    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
    2.59 +      (theory_context (Thm.theory_of_thm st) ss) i st
    2.60 +  end;
    2.61 +
    2.62  (*Prunes all redundant parameters from the proof state by rewriting.
    2.63    DOES NOT rewrite main goal, where quantification over an unused bound
    2.64      variable is sometimes done to avoid the need for cut_facts_tac.*)

     3.1 --- a/src/Pure/simplifier.ML	Tue Jul 03 17:17:09 2007 +0200
     3.2 +++ b/src/Pure/simplifier.ML	Tue Jul 03 17:17:11 2007 +0200
     3.3 @@ -260,7 +260,7 @@
     3.4        (rev (if safe then solvers else unsafe_solvers)));
     3.5  
     3.6      fun simp_loop_tac i =
     3.7 -      Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
     3.8 +      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
     3.9        (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
    3.10    in simp_loop_tac end;
    3.11