tuned signature;

--- a/src/Pure/raw_simplifier.ML	Tue Feb 14 19:18:57 2012 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Feb 14 19:29:54 2012 +0100
@@ -123,7 +123,7 @@
   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 asm_rewrite_goal_tac: bool * bool * bool ->
+  val generic_rewrite_goal_tac: bool * bool * bool ->
     (simpset -> tactic) -> simpset -> int -> tactic
   val rewrite: bool -> thm list -> conv
   val simplify: bool -> thm list -> thm -> thm
@@ -1298,14 +1298,14 @@
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 
 (*Rewrite one subgoal*)
-fun asm_rewrite_goal_tac mode prover_tac ss i thm =
+fun generic_rewrite_goal_tac mode prover_tac ss i thm =
   if 0 < i andalso i <= Thm.nprems_of thm then
     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
   else Seq.empty;
 
 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)
+    fn i => fn st => generic_rewrite_goal_tac (true, false, false) (K no_tac)
       (global_context (Thm.theory_of_thm st) ss) i st
   end;
 

--- a/src/Pure/simplifier.ML	Tue Feb 14 19:18:57 2012 +0100
+++ b/src/Pure/simplifier.ML	Tue Feb 14 19:29:54 2012 +0100
@@ -239,7 +239,7 @@
       (rev (if safe then solvers else unsafe_solvers)));
 
     fun simp_loop_tac i =
-      Raw_Simplifier.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
+      Raw_Simplifier.generic_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;