# HG changeset patch
# User berghofe
# Date 1012920688 -3600
# Node ID cdf338ef5fadd7002d1ef438ce75db5f20e079e2
# Parent  5c900a821a7c3b72d96110a3a22fa6bc024316f3
New function maxidx_of_proof.

diff -r 5c900a821a7c -r cdf338ef5fad src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Feb 04 13:16:54 2002 +0100
+++ b/src/Pure/proofterm.ML	Tue Feb 05 15:51:28 2002 +0100
@@ -46,6 +46,7 @@
   val add_prf_names : string list * proof -> string list
   val add_prf_tfree_names : string list * proof -> string list
   val add_prf_tvar_ixns : indexname list * proof -> indexname list
+  val maxidx_of_proof : proof -> int
   val prf_abstract_over : term -> proof -> proof
   val prf_incr_bv : int -> int -> int -> int -> proof -> proof
   val incr_pboundvars : int -> int -> proof -> proof
@@ -264,6 +265,9 @@
 val add_prf_tfree_names = fold_proof_terms add_term_tfree_names add_typ_tfree_names;
 val add_prf_tvar_ixns = fold_proof_terms add_term_tvar_ixns (add_typ_ixns o swap);
 
+fun maxidx_of_proof prf = fold_proof_terms
+  (Int.max o apfst maxidx_of_term) (Int.max o apfst maxidx_of_typ) (~1, prf); 
+
 
 (***** utilities *****)