# 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))