# HG changeset patch
# User berghofe
# Date 1000391176 -7200
# Node ID e172cbed431d849042c761d520368eed42e130fa
# Parent  804ee65ee1a183bf7ee956f098005549e9970b43
Fixed proof term bug in permute_prems.

diff -r 804ee65ee1a1 -r e172cbed431d src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Sep 12 18:10:52 2001 +0200
+++ b/src/Pure/thm.ML	Thu Sep 13 16:26:16 2001 +0200
@@ -1112,7 +1112,8 @@
       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
+      val m      = if k<0 then n+k else k
+      val Bi'    = if 0=m orelse m=n then Bi
 		   else if 0<m andalso m<n 
 		   then list_all 
 			   (params, 
@@ -1122,12 +1123,11 @@
 		   else raise THM("rotate_rule", k, [state])
   in  (*no fix_shyps*)
       Thm{sign_ref = sign_ref, 
-          der = Pt.infer_derivs'
-            (Pt.rotate_proof Bs Bi (if k<0 then n+k else k)) der,
+          der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
 	  maxidx = maxidx,
 	  shyps = shyps,
 	  hyps = hyps,
-	  prop = Logic.rule_of(tpairs, Bs@[rot (if k<0 then n+k else k)], C)}
+	  prop = Logic.rule_of (tpairs, Bs @ [Bi'], C)}
   end;
 
 
@@ -1142,7 +1142,8 @@
       and fixed_prems = List.take(prems, j)
         handle Subscript => raise THM("permute_prems:j", j, [rl])
       val n_j    = length moved_prems
-      fun rot m  = if 0 = m orelse m = n_j then prop
+      val m = if k<0 then n_j + k else k
+      val prop'  = if 0 = m orelse m = n_j then prop
 		   else if 0<m andalso m<n_j 
 		   then Logic.list_implies(fixed_prems @
 					   List.drop(moved_prems, m) @ 
@@ -1151,11 +1152,11 @@
 		   else raise THM("permute_prems:k", k, [rl])
   in  (*no fix_shyps*)
       Thm{sign_ref = sign_ref, 
-          der = Pt.infer_derivs' (Pt.permute_prems_prf prems j k) der,
+          der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
 	  maxidx = maxidx,
 	  shyps = shyps,
 	  hyps = hyps,
-	  prop = rot (if k<0 then n_j + k else k)}
+	  prop = prop'}
   end;