# HG changeset patch
# User wenzelm
# Date 1193414133 -7200
# Node ID e5b2dd8db7c88a060ebde6366519c07080ac13ec
# Parent  3a539d9995fb3c962295d755e9b719a0d6372709
asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;

diff -r 3a539d9995fb -r e5b2dd8db7c8 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Oct 26 17:18:32 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Oct 26 17:55:33 2007 +0200
@@ -1285,8 +1285,10 @@
 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 asm_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