# HG changeset patch
# User wenzelm
# Date 1154287736 -7200
# Node ID fd0ed14ba1eafbae230ddcf7be915fcaffd81f75
# Parent  ef3ee6a91c181a6f837544b4da2c01d2703ddb6c
added maxidx_values;

diff -r ef3ee6a91c18 -r fd0ed14ba1ea src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun Jul 30 21:28:55 2006 +0200
+++ b/src/Pure/Isar/args.ML	Sun Jul 30 21:28:56 2006 +0200
@@ -29,6 +29,7 @@
   val map_name: (string -> string) -> src -> src
   val map_values: (string -> string) -> (typ -> typ) -> (term -> term) -> (thm -> thm)
     -> src -> src
+  val maxidx_values: src -> int -> int
   val assignable: src -> src
   val assign: value option -> T -> unit
   val closure: src -> src
@@ -178,6 +179,12 @@
     | Fact ths => Fact (map i ths)
     | Attribute att => Attribute att));
 
+fun maxidx_values (Src ((_, args), _)) = args |> fold
+  (fn (Arg (_, Value (SOME (Typ T)))) => Term.maxidx_typ T
+    | (Arg (_, Value (SOME (Term t)))) => Term.maxidx_term t
+    | (Arg (_, Value (SOME (Fact ths)))) => fold Thm.maxidx_thm ths
+    | _ => I);
+
 
 (* static binding *)