Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
authorwenzelm
Fri, 26 Oct 2007 17:55:33 +0200
changeset 25203 e5b2dd8db7c8
parent 25202 3a539d9995fb
child 25204 36cf92f63a44
asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle