# HG changeset patch
# User wenzelm
# Date 1154550414 -7200
# Node ID 963bf056e8f7ed2aecfdefae5a88bb15271ad316
# Parent  5330f710b9607c7302f9297ed4f6d7d0b4231af8
replaced maxidx_of_proof by maxidx_proof;

diff -r 5330f710b960 -r 963bf056e8f7 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Aug 02 22:26:53 2006 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 02 22:26:54 2006 +0200
@@ -43,7 +43,7 @@
   val map_proof_terms_option : (term -> term option) -> (typ -> typ option) -> proof -> proof
   val map_proof_terms : (term -> term) -> (typ -> typ) -> proof -> proof
   val fold_proof_terms : (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
-  val maxidx_of_proof : proof -> int
+  val maxidx_proof : proof -> int -> int
   val size_of_proof : proof -> int
   val change_type : typ list option -> proof -> proof
   val prf_abstract_over : term -> proof -> proof
@@ -308,7 +308,7 @@
   | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
   | fold_proof_terms _ _ _ = I;
 
-fun maxidx_of_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf ~1;
+fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf;
 
 fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
   | size_of_proof (AbsP (_, t, prf)) = 1 + size_of_proof prf