# HG changeset patch
# User wenzelm
# Date 1273328684 -7200
# Node ID 6f8bbe9ca8a295f66532b33c59d92ea48a35e556
# Parent  d65ed9d7275e369fb440868a2a794407099cbdcf
tuned signature;

diff -r d65ed9d7275e -r 6f8bbe9ca8a2 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat May 08 16:03:09 2010 +0200
+++ b/src/Pure/proofterm.ML	Sat May 08 16:24:44 2010 +0200
@@ -84,7 +84,7 @@
   val varify_proof: term -> (string * sort) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> int -> proof -> proof
-  val permute_prems_prf: term list -> int -> int -> proof -> proof
+  val permute_prems_proof: term list -> int -> int -> proof -> proof
   val generalize: string list * string list -> int -> proof -> proof
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> proof -> proof
@@ -695,7 +695,7 @@
 
 (***** permute premises *****)
 
-fun permute_prems_prf prems j k prf =
+fun permute_prems_proof prems j k prf =
   let val n = length prems
   in mk_AbsP (n, proof_combP (prf,
     map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
diff -r d65ed9d7275e -r 6f8bbe9ca8a2 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat May 08 16:03:09 2010 +0200
+++ b/src/Pure/thm.ML	Sat May 08 16:24:44 2010 +0200
@@ -1436,7 +1436,7 @@
         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
-    Thm (deriv_rule1 (Pt.permute_prems_prf prems j m) der,
+    Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,