# HG changeset patch # User bulwahn # Date 1285667997 -7200 # Node ID 66c1e526fd44acba708dc94a4c07cf30961f9139 # Parent 19cb8d5581666bbaae02d199d5c2c07912c6eb61 avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead diff -r 19cb8d558166 -r 66c1e526fd44 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 11:59:53 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 28 11:59:57 2010 +0200 @@ -2404,9 +2404,10 @@ @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 THEN (if (is_some name) then print_tac options "before applying not introduction rule" - THEN rotate_tac premposition 1 - THEN etac (the neg_intro_rule) 1 - THEN rotate_tac (~premposition) 1 + THEN Subgoal.FOCUS_PREMS + (fn {context = ctxt, params = params, prems, asms, concl, schematics} => + rtac (the neg_intro_rule) 1 + THEN rtac (nth prems premposition) 1) ctxt 1 THEN print_tac options "after applying not introduction rule" THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations)) THEN (REPEAT_DETERM (atac 1))