# HG changeset patch
# User paulson
# Date 945360076 -3600
# Node ID 54d37e491ac2e30ce71449f5031bd19799332dcc
# Parent  658e0d4e4ed9406515cbf5dacd7af882ce86e0a0
SOUNDNESS BUG FIX for rotate_rule.  The original code did not expect
nested parameters such as !!y.

Goal "!!x. x = a ==> (!!y. y ~= a ==> False)";
by (rotate_tac 1 1);
be notE 1;
ba 1;
qed "foo";

val FalseI = standard (True_not_False RS (standard (refl RS foo)));

diff -r 658e0d4e4ed9 -r 54d37e491ac2 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Dec 15 10:45:37 1999 +0100
+++ b/src/Pure/thm.ML	Thu Dec 16 17:01:16 1999 +0100
@@ -1230,9 +1230,10 @@
 fun rotate_rule k i state =
   let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state;
       val (tpairs, Bs, Bi, C) = dest_state(state,i)
-      val params = Logic.strip_params Bi
-      and asms   = Logic.strip_assums_hyp Bi
-      and concl  = Logic.strip_assums_concl Bi
+      val params = Term.strip_all_vars Bi
+      and rest   = Term.strip_all_body Bi
+      val asms   = Logic.strip_imp_prems rest
+      and concl  = Logic.strip_imp_concl rest
       val n      = length asms
       fun rot m  = if 0=m orelse m=n then Bi
 		   else if 0<m andalso m<n