1.1 --- a/src/Pure/raw_simplifier.ML	Tue Feb 14 19:18:57 2012 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Tue Feb 14 19:29:54 2012 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4    val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
     1.5    val rewrite_thm: bool * bool * bool ->
     1.6      (simpset -> thm -> thm option) -> simpset -> thm -> thm
     1.7 -  val asm_rewrite_goal_tac: bool * bool * bool ->
     1.8 +  val generic_rewrite_goal_tac: bool * bool * bool ->
     1.9      (simpset -> tactic) -> simpset -> int -> tactic
    1.10    val rewrite: bool -> thm list -> conv
    1.11    val simplify: bool -> thm list -> thm -> thm
    1.12 @@ -1298,14 +1298,14 @@
    1.13  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.14  
    1.15  (*Rewrite one subgoal*)
    1.16 -fun asm_rewrite_goal_tac mode prover_tac ss i thm =
    1.17 +fun generic_rewrite_goal_tac mode prover_tac ss i thm =
    1.18    if 0 < i andalso i <= Thm.nprems_of thm then
    1.19      Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
    1.20    else Seq.empty;
    1.21  
    1.22  fun rewrite_goal_tac rews =
    1.23    let val ss = empty_ss addsimps rews in
    1.24 -    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.25 +    fn i => fn st => generic_rewrite_goal_tac (true, false, false) (K no_tac)
    1.26        (global_context (Thm.theory_of_thm st) ss) i st
    1.27    end;
    1.28  

     2.1 --- a/src/Pure/simplifier.ML	Tue Feb 14 19:18:57 2012 +0100
     2.2 +++ b/src/Pure/simplifier.ML	Tue Feb 14 19:29:54 2012 +0100
     2.3 @@ -239,7 +239,7 @@
     2.4        (rev (if safe then solvers else unsafe_solvers)));
     2.5  
     2.6      fun simp_loop_tac i =
     2.7 -      Raw_Simplifier.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
     2.8 +      Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
     2.9        (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
    2.10    in simp_loop_tac end;
    2.11