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 =