# HG changeset patch
# User wenzelm
# Date 1425739236 -3600
# Node ID 48d400469bcbaaaee29e5bc204d563f104b15aee
# Parent  f89464e9ffa056ab6162310372ec4f81a4462e32
added declare_maxidx operations for Eisbach;

diff -r f89464e9ffa0 -r 48d400469bcb src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat Mar 07 12:32:55 2015 +0100
+++ b/src/Pure/Isar/token.ML	Sat Mar 07 15:40:36 2015 +0100
@@ -72,6 +72,8 @@
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val reports_of_value: T -> Position.report list
+  val declare_maxidx: T -> Proof.context -> Proof.context
+  val declare_maxidx_src: src -> Proof.context -> Proof.context
   val transform: morphism -> T -> T
   val transform_src: morphism -> src -> src
   val init_assignable: T -> T
@@ -404,6 +406,23 @@
   | _ => []);
 
 
+(* maxidx *)
+
+fun declare_maxidx tok =
+  (case get_value tok of
+    SOME (Source src) => declare_maxidx_src src
+  | SOME (Typ T) => Variable.declare_maxidx (Term.maxidx_of_typ T)
+  | SOME (Term t) => Variable.declare_maxidx (Term.maxidx_of_term t)
+  | SOME (Fact (_, ths)) => fold (Variable.declare_maxidx o Thm.maxidx_of) ths
+  | SOME (Attribute _) => I  (* FIXME !? *)
+  | SOME (Declaration decl) =>
+      (fn ctxt =>
+        let val ctxt' = Context.proof_map (Morphism.form decl) ctxt
+        in Variable.declare_maxidx (Variable.maxidx_of ctxt') ctxt end)
+  | _ => I)
+and declare_maxidx_src src = fold declare_maxidx (args_of_src src);
+
+
 (* transform *)
 
 fun transform phi =
diff -r f89464e9ffa0 -r 48d400469bcb src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Mar 07 12:32:55 2015 +0100
+++ b/src/Pure/variable.ML	Sat Mar 07 15:40:36 2015 +0100
@@ -19,6 +19,7 @@
   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
@@ -207,6 +208,11 @@
 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 =