src/Pure/variable.ML

   val is_declared: Proof.context -> string -> bool
   val check_name: binding -> string
   val default_type: Proof.context -> string -> typ option
   val def_type: Proof.context -> bool -> indexname -> typ option
   val def_sort: Proof.context -> indexname -> sort option
+  val declare_maxidx: int -> Proof.context -> Proof.context
   val declare_names: term -> Proof.context -> Proof.context
   val declare_constraints: term -> Proof.context -> Proof.context
   val declare_term: term -> Proof.context -> Proof.context
   val declare_typ: typ -> Proof.context -> Proof.context
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context

   end;
 
 val def_sort = Vartab.lookup o #2 o constraints_of;
 
 
+(* maxidx *)
+
+val declare_maxidx = map_maxidx o Integer.max;
+
+
 (* names *)
 
 fun declare_type_names t =
   map_names (fold_types (fold_atyps Term.declare_typ_names) t) #>
   map_maxidx (fold_types Term.maxidx_typ t);