# HG changeset patch
# User wenzelm
# Date 1144922467 -7200
# Node ID e425e74b01aff20b2c68194b4ec48b4d450807e5
# Parent  43bfe55759b0b4620ee4623d287f62c9314f5a60
added maxidx_of;

diff -r 43bfe55759b0 -r e425e74b01af src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Apr 13 12:01:06 2006 +0200
+++ b/src/Pure/thm.ML	Thu Apr 13 12:01:07 2006 +0200
@@ -75,6 +75,7 @@
   val eq_thms: thm list * thm list -> bool
   val theory_of_thm: thm -> theory
   val sign_of_thm: thm -> theory    (*obsolete*)
+  val maxidx_of: thm -> int
   val prop_of: thm -> term
   val proof_of: thm -> Proofterm.proof
   val tpairs_of: thm -> (term * term) list
@@ -443,6 +444,7 @@
 fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref;
 val sign_of_thm = theory_of_thm;
 
+fun maxidx_of (Thm {maxidx, ...}) = maxidx;
 fun prop_of (Thm {prop, ...}) = prop;
 fun proof_of (Thm {der = (_, proof), ...}) = proof;
 fun tpairs_of (Thm {tpairs, ...}) = tpairs;