tuned signature;
authorwenzelm
Sat May 08 16:24:44 2010 +0200 (2010-05-08 ago)
changeset 367426f8bbe9ca8a2
parent 36741 d65ed9d7275e
child 36743 ce2297415b54
tuned signature;
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/proofterm.ML	Sat May 08 16:03:09 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Sat May 08 16:24:44 2010 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4    val varify_proof: term -> (string * sort) list -> proof -> proof
     1.5    val legacy_freezeT: term -> proof -> proof
     1.6    val rotate_proof: term list -> term -> int -> proof -> proof
     1.7 -  val permute_prems_prf: term list -> int -> int -> proof -> proof
     1.8 +  val permute_prems_proof: term list -> int -> int -> proof -> proof
     1.9    val generalize: string list * string list -> int -> proof -> proof
    1.10    val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.11      -> proof -> proof
    1.12 @@ -695,7 +695,7 @@
    1.13  
    1.14  (***** permute premises *****)
    1.15  
    1.16 -fun permute_prems_prf prems j k prf =
    1.17 +fun permute_prems_proof prems j k prf =
    1.18    let val n = length prems
    1.19    in mk_AbsP (n, proof_combP (prf,
    1.20      map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
     2.1 --- a/src/Pure/thm.ML	Sat May 08 16:03:09 2010 +0200
     2.2 +++ b/src/Pure/thm.ML	Sat May 08 16:24:44 2010 +0200
     2.3 @@ -1436,7 +1436,7 @@
     2.4          in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
     2.5        else raise THM ("permute_prems: k", k, [rl]);
     2.6    in
     2.7 -    Thm (deriv_rule1 (Pt.permute_prems_prf prems j m) der,
     2.8 +    Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der,
     2.9       {thy_ref = thy_ref,
    2.10        tags = [],
    2.11        maxidx = maxidx,