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