replaced maxidx_of_proof by maxidx_proof;
authorwenzelm
Wed Aug 02 22:26:54 2006 +0200 (2006-08-02)
changeset 20300963bf056e8f7
parent 20299 5330f710b960
child 20301 66b2a1f16bbb
replaced maxidx_of_proof by maxidx_proof;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Wed Aug 02 22:26:53 2006 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Aug 02 22:26:54 2006 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    val map_proof_terms_option : (term -> term option) -> (typ -> typ option) -> proof -> proof
     1.5    val map_proof_terms : (term -> term) -> (typ -> typ) -> proof -> proof
     1.6    val fold_proof_terms : (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
     1.7 -  val maxidx_of_proof : proof -> int
     1.8 +  val maxidx_proof : proof -> int -> int
     1.9    val size_of_proof : proof -> int
    1.10    val change_type : typ list option -> proof -> proof
    1.11    val prf_abstract_over : term -> proof -> proof
    1.12 @@ -308,7 +308,7 @@
    1.13    | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
    1.14    | fold_proof_terms _ _ _ = I;
    1.15  
    1.16 -fun maxidx_of_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf ~1;
    1.17 +fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf;
    1.18  
    1.19  fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
    1.20    | size_of_proof (AbsP (_, t, prf)) = 1 + size_of_proof prf