1.1 --- a/src/Pure/Isar/args.ML	Sat Mar 13 20:34:22 2010 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Sat Mar 13 20:44:12 2010 +0100
     1.3 @@ -14,7 +14,6 @@
     1.4    val pretty_src: Proof.context -> src -> Pretty.T
     1.5    val map_name: (string -> string) -> src -> src
     1.6    val morph_values: morphism -> src -> src
     1.7 -  val maxidx_values: src -> int -> int
     1.8    val assignable: src -> src
     1.9    val closure: src -> src
    1.10    val context: Proof.context context_parser
    1.11 @@ -111,13 +110,6 @@
    1.12      | T.Fact ths => T.Fact (Morphism.fact phi ths)
    1.13      | T.Attribute att => T.Attribute (Morphism.transform phi att)));
    1.14  
    1.15 -fun maxidx_values (Src ((_, args), _)) = args |> fold (fn arg =>
    1.16 -  (case T.get_value arg of
    1.17 -    SOME (T.Typ T) => Term.maxidx_typ T
    1.18 -  | SOME (T.Term t) => Term.maxidx_term t
    1.19 -  | SOME (T.Fact ths) => fold Thm.maxidx_thm ths
    1.20 -  | _ => I));
    1.21 -
    1.22  val assignable = map_args T.assignable;
    1.23  val closure = map_args T.closure;
    1.24