1.1 --- a/src/Pure/meta_simplifier.ML	Fri Oct 26 17:18:32 2007 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Oct 26 17:55:33 2007 +0200
     1.3 @@ -1285,8 +1285,10 @@
     1.4  fun rewtac def = rewrite_goals_tac [def];
     1.5  
     1.6  (*Rewrite subgoal i only.*)
     1.7 -fun asm_rewrite_goal_tac mode prover_tac ss i =
     1.8 -  PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) ss i);
     1.9 +fun asm_rewrite_goal_tac mode prover_tac ss i thm =
    1.10 +  if 0 < i andalso i <= Thm.nprems_of thm then
    1.11 +    Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
    1.12 +  else Seq.empty;
    1.13  
    1.14  fun rewrite_goal_tac rews =
    1.15    let val ss = empty_ss addsimps rews in