# HG changeset patch
# User wenzelm
# Date 1183475831 -7200
# Node ID 60a1672e298e37fa9526e0a6e8cf33229e425c50
# Parent  58147e5bd070f6a10c81e237a2f22ae50928faf0
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);

diff -r 58147e5bd070 -r 60a1672e298e src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Jul 03 17:17:09 2007 +0200
+++ b/src/Pure/goal.ML	Tue Jul 03 17:17:11 2007 +0200
@@ -32,8 +32,6 @@
   val conjunction_tac: int -> tactic
   val precise_conjunction_tac: int -> int -> tactic
   val recover_conjunction_tac: tactic
-  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
-  val rewrite_goal_tac: thm list -> int -> tactic
   val norm_hhf_tac: int -> tactic
   val compose_hhf: thm -> int -> thm -> thm Seq.seq
   val compose_hhf_tac: thm -> int -> tactic
@@ -209,27 +207,13 @@
     THEN recover_conjunction_tac);
 
 
-(* rewriting *)
-
-(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
-fun asm_rewrite_goal_tac mode prover_tac ss =
-  SELECT_GOAL
-    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
-
-fun rewrite_goal_tac rews =
-  let val ss = MetaSimplifier.empty_ss addsimps rews in
-    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
-      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
-  end;
-
-
 (* hhf normal form *)
 
 val norm_hhf_tac =
   rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   THEN' SUBGOAL (fn (t, i) =>
     if Drule.is_norm_hhf t then all_tac
-    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
+    else MetaSimplifier.rewrite_goal_tac [Drule.norm_hhf_eq] i);
 
 fun compose_hhf tha i thb =
   Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
diff -r 58147e5bd070 -r 60a1672e298e src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Tue Jul 03 17:17:09 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Jul 03 17:17:11 2007 +0200
@@ -81,6 +81,7 @@
   val rewrite_goals_rule: thm list -> thm -> thm
   val rewrite_goals_tac: thm list -> tactic
   val rewrite_tac: thm list -> tactic
+  val rewrite_goal_tac: thm list -> int -> tactic
   val rewtac: thm -> tactic
   val prune_params_tac: tactic
   val fold_rule: thm list -> thm -> thm
@@ -113,6 +114,8 @@
     (simpset -> thm -> thm option) -> simpset -> thm -> thm
   val rewrite_goal_rule: bool * bool * bool ->
     (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
+  val asm_rewrite_goal_tac: bool * bool * bool ->
+    (simpset -> tactic) -> simpset -> int -> tactic
   val norm_hhf: thm -> thm
   val norm_hhf_protect: thm -> thm
   val rewrite: bool -> thm list -> cterm -> thm
@@ -1266,27 +1269,37 @@
 
 fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
 
-(*Rewrite the subgoals of a proof state (represented by a theorem) *)
+(*Rewrite the subgoals of a proof state (represented by a theorem)*)
 fun rewrite_goals_rule thms th =
-  Conv.fconv_rule (Conv.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover
-    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
+  Conv.fconv_rule (Conv.prems_conv ~1 (K (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)*)
 fun rewrite_goal_rule mode prover ss i thm =
-  if 0 < i  andalso  i <= nprems_of thm
-  then Conv.fconv_rule (Conv.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
-  else raise THM("rewrite_goal_rule", i, [thm]);
+  if 0 < i andalso i <= Thm.nprems_of thm
+  then Conv.goal_conv_rule (rewrite_cterm mode prover ss) i thm
+  else raise THM ("rewrite_goal_rule", i, [thm]);
 
 
 (** meta-rewriting tactics **)
 
 (*Rewrite throughout proof state. *)
-fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
+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];
 
+(*Rewrite subgoal i only.*)
+fun asm_rewrite_goal_tac mode prover_tac ss i =
+  PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) ss i);
+
+fun rewrite_goal_tac rews =
+  let val ss = empty_ss addsimps rews in
+    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
+      (theory_context (Thm.theory_of_thm st) ss) i st
+  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.*)
diff -r 58147e5bd070 -r 60a1672e298e src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Jul 03 17:17:09 2007 +0200
+++ b/src/Pure/simplifier.ML	Tue Jul 03 17:17:11 2007 +0200
@@ -260,7 +260,7 @@
       (rev (if safe then solvers else unsafe_solvers)));
 
     fun simp_loop_tac i =
-      Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
+      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   in simp_loop_tac end;