diff --git a/src/Pure/General/symbol.ML b/src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML
+++ b/src/Pure/General/symbol.ML
@@ -1,519 +1,517 @@
 (*  Title:      Pure/General/symbol.ML
     Author:     Makarius
 
 Isabelle text symbols.
 *)
 
 signature SYMBOL =
 sig
   type symbol = string
   val explode: string -> symbol list
   val spaces: int -> string
   val STX: symbol
   val DEL: symbol
   val open_: symbol
   val close: symbol
   val space: symbol
   val is_space: symbol -> bool
   val comment: symbol
   val cancel: symbol
   val latex: symbol
   val marker: symbol
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
   val is_symbolic_char: symbol -> bool
   val is_printable: symbol -> bool
   val control_prefix: string
   val control_suffix: string
   val is_control: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
   val stopper: symbol Scan.stopper
   val is_malformed: symbol -> bool
   val malformed_msg: symbol -> string
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
   val is_ascii_digit: symbol -> bool
   val is_ascii_hex: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
   val is_ascii_line_terminator: symbol -> bool
   val is_ascii_control: symbol -> bool
   val is_ascii_letdig: symbol -> bool
   val is_ascii_lower: symbol -> bool
   val is_ascii_upper: symbol -> bool
   val to_ascii_lower: symbol -> symbol
   val to_ascii_upper: symbol -> symbol
   val is_ascii_identifier: string -> bool
   val scan_ascii_id: string list -> string * string list
   datatype sym =
     Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF
   val decode: symbol -> sym
   val encode: sym -> symbol
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
   val is_letter: symbol -> bool
   val is_digit: symbol -> bool
   val is_quasi: symbol -> bool
   val is_blank: symbol -> bool
   val is_control_block: symbol -> bool
   val has_control_block: symbol list -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val beginning: int -> symbol list -> string
   val esc: symbol -> string
   val escape: string -> string
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val split_words: symbol list -> string list
   val explode_words: string -> string list
   val trim_blanks: string -> string
   val bump_init: string -> string
   val bump_string: string -> string
   val sub: symbol
   val sup: symbol
   val bold: symbol
   val make_sub: string -> string
   val make_sup: string -> string
   val make_bold: string -> string
   val length: symbol list -> int
   val output: string -> Output.output * int
 end;
 
 structure Symbol: SYMBOL =
 struct
 
 (** type symbol **)
 
 (*Symbols, which are considered the smallest entities of any Isabelle
   string, may be of the following form:
 
     (1) ASCII: a
     (2) UTF-8: ä
     (2) regular symbols: \<ident>
     (3) control symbols: \<^ident>
 
   Output is subject to the print_mode variable (default: verbatim),
   actual interpretation in display is up to front-end tools.
 *)
 
 type symbol = string;
 
 val STX = chr 2;
 val DEL = chr 127;
 
 val open_ = "\<open>";
 val close = "\<close>";
 
 val space = chr 32;
 fun is_space s = s = space;
 
 local
-  val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
+  val spaces0 = Vector.tabulate (65, fn i => replicate_string i space);
 in
   fun spaces n =
-    if n < 64 then Vector.sub (small_spaces, n)
-    else
-      replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^
-        Vector.sub (small_spaces, n mod 64);
+    if n < 64 then Vector.nth spaces0 n
+    else replicate_string (n div 64) (Vector.nth spaces0 64) ^ Vector.nth spaces0 (n mod 64);
 end;
 
 val comment = "\<comment>";
 val cancel = "\<^cancel>";
 val latex = "\<^latex>";
 val marker = "\<^marker>";
 
 fun is_char s = size s = 1;
 
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
 
 fun raw_symbolic s =
   String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);
 
 fun is_symbolic s =
   s <> open_ andalso s <> close andalso raw_symbolic s;
 
 val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
 
 fun is_printable s =
   if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~"
   else is_utf8 s orelse raw_symbolic s;
 
 val control_prefix = "\092<^";
 val control_suffix = ">";
 
 fun is_control s =
   String.isPrefix control_prefix s andalso String.isSuffix control_suffix s;
 
 
 (* input source control *)
 
 val eof = "";
 fun is_eof s = s = eof;
 fun not_eof s = s <> eof;
 val stopper = Scan.stopper (K eof) is_eof;
 
 fun is_malformed s =
   String.isPrefix "\092<" s andalso not (String.isSuffix ">" s)
   orelse s = "\092<>" orelse s = "\092<^>";
 
 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
 
 (* ASCII symbols *)
 
 fun is_ascii s = is_char s andalso ord s < 128;
 
 fun is_ascii_letter s =
   is_char s andalso
    (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z" orelse
     Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
 
 fun is_ascii_digit s =
   is_char s andalso Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9";
 
 fun is_ascii_hex s =
   is_char s andalso
    (Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9" orelse
     Char.ord #"A" <= ord s andalso ord s <= Char.ord #"F" orelse
     Char.ord #"a" <= ord s andalso ord s <= Char.ord #"f");
 
 fun is_ascii_quasi "_" = true
   | is_ascii_quasi "'" = true
   | is_ascii_quasi _ = false;
 
 val is_ascii_blank =
   fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true
     | _ => false;
 
 val is_ascii_line_terminator =
   fn "\r" => true | "\n" => true | _ => false;
 
 fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
 
 fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;
 
 fun is_ascii_lower s = is_char s andalso (Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
 fun is_ascii_upper s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z");
 
 fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + Char.ord #"a" - Char.ord #"A") else s;
 fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + Char.ord #"A" - Char.ord #"a") else s;
 
 fun is_ascii_identifier s =
   size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso
   forall_string is_ascii_letdig s;
 
 val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode);
 
 
 (* diagnostics *)
 
 fun beginning n cs =
   let
     val drop_blanks = drop_suffix is_ascii_blank;
     val all_cs = drop_blanks cs;
     val dots = if length all_cs > n then " ..." else "";
   in
     (drop_blanks (take n all_cs)
       |> map (fn c => if is_ascii_blank c then space else c)
       |> implode) ^ dots
   end;
 
 
 (* symbol variants *)
 
 datatype sym =
   Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF;
 
 fun decode s =
   if s = "" then EOF
   else if is_char s then Char s
   else if is_utf8 s then UTF8 s
   else if is_malformed s then Malformed s
   else if is_control s then Control (String.substring (s, 3, size s - 4))
   else Sym (String.substring (s, 2, size s - 3));
 
 fun encode (Char s) = s
   | encode (UTF8 s) = s
   | encode (Sym s) = "\092<" ^ s ^ ">"
   | encode (Control s) = "\092<^" ^ s ^ ">"
   | encode (Malformed s) = s
   | encode EOF = "";
 
 
 (* standard symbol kinds *)
 
 local
   val letter_symbols =
     Symset.make [
       "\<A>",
       "\<B>",
       "\<C>",
       "\<D>",
       "\<E>",
       "\<F>",
       "\<G>",
       "\<H>",
       "\<I>",
       "\<J>",
       "\<K>",
       "\<L>",
       "\<M>",
       "\<N>",
       "\<O>",
       "\<P>",
       "\<Q>",
       "\<R>",
       "\<S>",
       "\<T>",
       "\<U>",
       "\<V>",
       "\<W>",
       "\<X>",
       "\<Y>",
       "\<Z>",
       "\<a>",
       "\<b>",
       "\<c>",
       "\<d>",
       "\<e>",
       "\<f>",
       "\<g>",
       "\<h>",
       "\<i>",
       "\<j>",
       "\<k>",
       "\<l>",
       "\<m>",
       "\<n>",
       "\<o>",
       "\<p>",
       "\<q>",
       "\<r>",
       "\<s>",
       "\<t>",
       "\<u>",
       "\<v>",
       "\<w>",
       "\<x>",
       "\<y>",
       "\<z>",
       "\<AA>",
       "\<BB>",
       "\<CC>",
       "\<DD>",
       "\<EE>",
       "\<FF>",
       "\<GG>",
       "\<HH>",
       "\<II>",
       "\<JJ>",
       "\<KK>",
       "\<LL>",
       "\<MM>",
       "\<NN>",
       "\<OO>",
       "\<PP>",
       "\<QQ>",
       "\<RR>",
       "\<SS>",
       "\<TT>",
       "\<UU>",
       "\<VV>",
       "\<WW>",
       "\<XX>",
       "\<YY>",
       "\<ZZ>",
       "\<aa>",
       "\<bb>",
       "\<cc>",
       "\<dd>",
       "\<ee>",
       "\<ff>",
       "\<gg>",
       "\<hh>",
       "\<ii>",
       "\<jj>",
       "\<kk>",
       "\<ll>",
       "\<mm>",
       "\<nn>",
       "\<oo>",
       "\<pp>",
       "\<qq>",
       "\<rr>",
       "\<ss>",
       "\<tt>",
       "\<uu>",
       "\<vv>",
       "\<ww>",
       "\<xx>",
       "\<yy>",
       "\<zz>",
       "\<alpha>",
       "\<beta>",
       "\<gamma>",
       "\<delta>",
       "\<epsilon>",
       "\<zeta>",
       "\<eta>",
       "\<theta>",
       "\<iota>",
       "\<kappa>",
       (*"\<lambda>", sic!*)
       "\<mu>",
       "\<nu>",
       "\<xi>",
       "\<pi>",
       "\<rho>",
       "\<sigma>",
       "\<tau>",
       "\<upsilon>",
       "\<phi>",
       "\<chi>",
       "\<psi>",
       "\<omega>",
       "\<Gamma>",
       "\<Delta>",
       "\<Theta>",
       "\<Lambda>",
       "\<Xi>",
       "\<Pi>",
       "\<Sigma>",
       "\<Upsilon>",
       "\<Phi>",
       "\<Psi>",
       "\<Omega>"
     ];
 in
 
 val is_letter_symbol = Symset.member letter_symbols;
 
 end;
 
 datatype kind = Letter | Digit | Quasi | Blank | Other;
 
 fun kind s =
   if is_ascii_letter s then Letter
   else if is_ascii_digit s then Digit
   else if is_ascii_quasi s then Quasi
   else if is_ascii_blank s then Blank
   else if is_char s then Other
   else if is_letter_symbol s then Letter
   else Other;
 
 fun is_letter s = kind s = Letter;
 fun is_digit s = kind s = Digit;
 fun is_quasi s = kind s = Quasi;
 fun is_blank s = kind s = Blank;
 
 val is_control_block = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
 val has_control_block = exists is_control_block;
 
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
 
 
 (* escape *)
 
 val esc = fn s =>
   if is_char s then s
   else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
   else "\\" ^ s;
 
 val escape = implode o map esc o Symbol.explode;
 
 
 
 (** scanning through symbols **)
 
 (* scanner *)
 
 fun scanner msg scan syms =
   let
     fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss))
       | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss));
     val finite_scan = Scan.error (Scan.finite stopper (!! message scan));
   in
     (case finite_scan syms of
       (result, []) => result
     | (_, rest) => error (message (rest, NONE) ()))
   end;
 
 
 (* space-separated words *)
 
 val scan_word =
   Scan.many1 is_ascii_blank >> K NONE ||
   Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode);
 
 val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);
 
 val explode_words = split_words o Symbol.explode;
 
 
 (* blanks *)
 
 val trim_blanks = Symbol.explode #> trim is_blank #> implode;
 
 
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\<^sub>" :: _) = true
   | symbolic_end ("'" :: ss) = symbolic_end ss
   | symbolic_end (s :: _) = raw_symbolic s
   | symbolic_end [] = false;
 
 fun bump_init str =
   if symbolic_end (rev (Symbol.explode str)) then str ^ "'"
   else str ^ "a";
 
 fun bump_string str =
   let
     fun bump [] = ["a"]
       | bump ("z" :: ss) = "a" :: bump ss
       | bump (s :: ss) =
           if is_char s andalso Char.ord #"a" <= ord s andalso ord s < Char.ord #"z"
           then chr (ord s + 1) :: ss
           else "a" :: s :: ss;
 
     val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str));
     val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   in implode (rev ss' @ qs) end;
 
 
 (* styles *)
 
 val sub = "\092<^sub>";
 val sup = "\092<^sup>";
 val bold = "\092<^bold>";
 
 fun make_style sym =
   Symbol.explode #> maps (fn s => [sym, s]) #> implode;
 
 val make_sub = make_style sub;
 val make_sup = make_style sup;
 val make_bold = make_style bold;
 
 
 
 (** symbol output **)
 
 (* length *)
 
 fun sym_len s =
   if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
   else if is_printable s then 1
   else 0;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
 
 fun output s = (s, sym_length (Symbol.explode s));
 
 
 (*final declarations of this structure!*)
 val explode = Symbol.explode;
 val length = sym_length;
 
 end;
diff --git a/src/Pure/General/vector.ML b/src/Pure/General/vector.ML
new file mode 100644
--- /dev/null
+++ b/src/Pure/General/vector.ML
@@ -0,0 +1,28 @@
+(*  Title:      Pure/General/vector.ML
+    Author:     Makarius
+
+Additional operations for structure Vector, following Isabelle/ML conventions.
+*)
+
+signature VECTOR =
+sig
+  include VECTOR
+  val nth: 'a vector -> int -> 'a
+  val forall: ('a -> bool) -> 'a vector -> bool
+  val fold: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
+  val fold_rev: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
+end;
+
+structure Vector: VECTOR =
+struct
+
+open Vector;
+
+fun nth vec i = sub (vec, i);
+
+val forall = all;
+
+fun fold f vec x = foldl (fn (a, b) => f a b) x vec;
+fun fold_rev f vec x = foldr (fn (a, b) => f a b) x vec;
+
+end;
diff --git a/src/Pure/Isar/token.ML b/src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML
+++ b/src/Pure/Isar/token.ML
@@ -1,802 +1,802 @@
 (*  Title:      Pure/Isar/token.ML
     Author:     Markus Wenzel, TU Muenchen
 
 Outer token syntax for Isabelle/Isar.
 *)
 
 signature TOKEN =
 sig
   datatype kind =
     (*immediate source*)
     Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
     Float | Space |
     (*delimited content*)
     String | Alt_String | Cartouche |
     Control of Antiquote.control |
     Comment of Comment.kind option |
     (*special content*)
     Error of string | EOF
   val control_kind: kind
   val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   type T
   type src = T list
   type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}
   datatype value =
     Source of src |
     Literal of bool * Markup.T |
     Name of name_value * morphism |
     Typ of typ |
     Term of term |
     Fact of string option * thm list |
     Attribute of morphism -> attribute |
     Declaration of declaration |
     Files of file Exn.result list |
     Output of XML.body option
   val pos_of: T -> Position.T
   val adjust_offsets: (int -> int option) -> T -> T
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
   val stopper: T Scan.stopper
   val kind_of: T -> kind
   val is_kind: kind -> T -> bool
   val get_control: T -> Antiquote.control option
   val is_command: T -> bool
   val keyword_with: (string -> bool) -> T -> bool
   val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool
   val is_comment: T -> bool
   val is_informal_comment: T -> bool
   val is_formal_comment: T -> bool
   val is_document_marker: T -> bool
   val is_ignored: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
   val is_error: T -> bool
   val is_space: T -> bool
   val is_blank: T -> bool
   val is_newline: T -> bool
   val range_of: T list -> Position.range
   val core_range_of: T list -> Position.range
   val content_of: T -> string
   val source_of: T -> string
   val input_of: T -> Input.source
   val inner_syntax_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
   val reports: Keyword.keywords -> T -> Position.report_text list
   val markups: Keyword.keywords -> T -> Markup.T list
   val unparse: T -> string
   val print: T -> string
   val text_of: T -> string * string
   val file_source: file -> Input.source
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
   val get_output: T -> XML.body option
   val put_output: XML.body -> T -> T
   val get_value: T -> value option
   val reports_of_value: T -> Position.report list
   val name_value: name_value -> value
   val get_name: T -> name_value option
   val declare_maxidx: T -> Proof.context -> Proof.context
   val map_facts: (string option -> thm list -> thm list) -> T -> T
   val trim_context_src: src -> src
   val transform: morphism -> T -> T
   val init_assignable: T -> T
   val assign: value option -> T -> T
   val evaluate: ('a -> value) -> (T -> 'a) -> T -> 'a
   val closure: T -> T
   val pretty_value: Proof.context -> T -> Pretty.T
   val name_of_src: src -> string * Position.T
   val args_of_src: src -> T list
   val checked_src: src -> bool
   val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a
   val pretty_src: Proof.context -> src -> Pretty.T
   val ident_or_symbolic: string -> bool
   val read_cartouche: Symbol_Pos.T list -> T
   val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list
   val explode: Keyword.keywords -> Position.T -> string -> T list
   val explode0: Keyword.keywords -> string -> T list
   val print_name: Keyword.keywords -> string -> string
   val print_properties: Keyword.keywords -> Properties.T -> string
   val make: (int * int) * string -> Position.T -> T * Position.T
   val make_string: string * Position.T -> T
   val make_int: int -> T list
   val make_src: string * Position.T -> T list -> src
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
 
 structure Token: TOKEN =
 struct
 
 (** tokens **)
 
 (* token kind *)
 
 datatype kind =
   (*immediate source*)
   Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
   Float | Space |
   (*delimited content*)
   String | Alt_String | Cartouche |
   Control of Antiquote.control |
   Comment of Comment.kind option |
   (*special content*)
   Error of string | EOF;
 
 val control_kind = Control Antiquote.no_control;
 
 fun equiv_kind kind kind' =
   (case (kind, kind') of
     (Control _, Control _) => true
   | (Error _, Error _) => true
   | _ => kind = kind');
 
 val str_of_kind =
  fn Command => "command"
   | Keyword => "keyword"
   | Ident => "identifier"
   | Long_Ident => "long identifier"
   | Sym_Ident => "symbolic identifier"
   | Var => "schematic variable"
   | Type_Ident => "type variable"
   | Type_Var => "schematic type variable"
   | Nat => "natural number"
   | Float => "floating-point number"
   | Space => "white space"
   | String => "quoted string"
   | Alt_String => "back-quoted string"
   | Cartouche => "text cartouche"
   | Control _ => "control cartouche"
   | Comment NONE => "informal comment"
   | Comment (SOME _) => "formal comment"
   | Error _ => "bad input"
   | EOF => "end-of-input";
 
 val immediate_kinds =
   Vector.fromList
     [Command, Keyword, Ident, Long_Ident, Sym_Ident, Var, Type_Ident, Type_Var, Nat, Float, Space];
 
 val delimited_kind =
   (fn String => true
     | Alt_String => true
     | Cartouche => true
     | Control _ => true
     | Comment _ => true
     | _ => false);
 
 
 (* datatype token *)
 
 (*The value slot assigns an (optional) internal value to a token,
   usually as a side-effect of special scanner setup (see also
   args.ML).  Note that an assignable ref designates an intermediate
   state of internalization -- it is NOT meant to persist.*)
 
 type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
 
 type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring};
 
 datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
 
 and slot =
   Slot |
   Value of value option |
   Assignable of value option Unsynchronized.ref
 
 and value =
   Source of T list |
   Literal of bool * Markup.T |
   Name of name_value * morphism |
   Typ of typ |
   Term of term |
   Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of morphism -> attribute |
   Declaration of declaration |
   Files of file Exn.result list |
   Output of XML.body option;
 
 type src = T list;
 
 
 (* position *)
 
 fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
 
 fun adjust_offsets adjust (Token ((x, range), y, z)) =
   Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
 
 
 (* stopper *)
 
 fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
 val eof = mk_eof Position.none;
 
 fun is_eof (Token (_, (EOF, _), _)) = true
   | is_eof _ = false;
 
 val not_eof = not o is_eof;
 
 val stopper =
   Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* kind of token *)
 
 fun kind_of (Token (_, (k, _), _)) = k;
 fun is_kind k (Token (_, (k', _), _)) = equiv_kind k k';
 
 fun get_control tok =
   (case kind_of tok of Control control => SOME control | _ => NONE);
 
 val is_command = is_kind Command;
 
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   | keyword_with _ _ = false;
 
 val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified");
 
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;
 
 fun is_ignored (Token (_, (Space, _), _)) = true
   | is_ignored (Token (_, (Comment NONE, _), _)) = true
   | is_ignored _ = false;
 
 fun is_proper (Token (_, (Space, _), _)) = false
   | is_proper (Token (_, (Comment _, _), _)) = false
   | is_proper _ = true;
 
 fun is_comment (Token (_, (Comment _, _), _)) = true
   | is_comment _ = false;
 
 fun is_informal_comment (Token (_, (Comment NONE, _), _)) = true
   | is_informal_comment _ = false;
 
 fun is_formal_comment (Token (_, (Comment (SOME _), _), _)) = true
   | is_formal_comment _ = false;
 
 fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true
   | is_document_marker _ = false;
 
 fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
   | is_begin_ignore _ = false;
 
 fun is_end_ignore (Token (_, (Comment NONE, ">"), _)) = true
   | is_end_ignore _ = false;
 
 fun is_error (Token (_, (Error _, _), _)) = true
   | is_error _ = false;
 
 
 (* blanks and newlines -- space tokens obey lines *)
 
 fun is_space (Token (_, (Space, _), _)) = true
   | is_space _ = false;
 
 fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
   | is_blank _ = false;
 
 fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
   | is_newline _ = false;
 
 
 (* range of tokens *)
 
 fun range_of (toks as tok :: _) =
       let val pos' = end_pos_of (List.last toks)
       in Position.range (pos_of tok, pos') end
   | range_of [] = Position.no_range;
 
 val core_range_of =
   drop_prefix is_ignored #> drop_suffix is_ignored #> range_of;
 
 
 (* token content *)
 
 fun content_of (Token (_, (_, x), _)) = x;
 fun source_of (Token ((source, _), _, _)) = source;
 
 fun input_of (Token ((source, range), (kind, _), _)) =
   Input.source (delimited_kind kind) source range;
 
 fun inner_syntax_of tok =
   let val x = content_of tok
   in if YXML.detect x then x else Syntax.implode_input (input_of tok) end;
 
 
 (* markup reports *)
 
 local
 
 val token_kind_markup =
  fn Var => (Markup.var, "")
   | Type_Ident => (Markup.tfree, "")
   | Type_Var => (Markup.tvar, "")
   | String => (Markup.string, "")
   | Alt_String => (Markup.alt_string, "")
   | Cartouche => (Markup.cartouche, "")
   | Control _ => (Markup.cartouche, "")
   | Comment _ => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
 
 fun command_markups keywords x =
   if Keyword.is_theory_end keywords x then [Markup.keyword2 |> Markup.keyword_properties]
   else
     (if Keyword.is_proof_asm keywords x then [Markup.keyword3]
      else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
      else [Markup.keyword1])
     |> map Markup.command_properties;
 
 in
 
 fun keyword_markup (important, keyword) x =
   if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
 
 fun completion_report tok =
   if is_kind Keyword tok
   then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
   else [];
 
 fun reports keywords tok =
   if is_command tok then
     keyword_reports tok (command_markups keywords (content_of tok))
   else if is_kind Keyword tok then
     keyword_reports tok
       [keyword_markup (false, Markup.keyword2 |> Markup.keyword_properties) (content_of tok)]
   else
     let
       val pos = pos_of tok;
       val (m, text) = token_kind_markup (kind_of tok);
       val deleted = Symbol_Pos.explode_deleted (source_of tok, pos);
     in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) deleted end;
 
 fun markups keywords = map (#2 o #1) o reports keywords;
 
 end;
 
 
 (* unparse *)
 
 fun unparse (Token (_, (kind, x), _)) =
   (case kind of
     String => Symbol_Pos.quote_string_qq x
   | Alt_String => Symbol_Pos.quote_string_bq x
   | Cartouche => cartouche x
   | Control control => Symbol_Pos.content (Antiquote.control_symbols control)
   | Comment NONE => enclose "(*" "*)" x
   | EOF => ""
   | _ => x);
 
 fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
 
 fun text_of tok =
   let
     val k = str_of_kind (kind_of tok);
     val ms = markups Keyword.empty_keywords tok;
     val s = unparse tok;
   in
     if s = "" then (k, "")
     else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
     then (k ^ " " ^ Markup.markups ms s, "")
     else (k, Markup.markups ms s)
   end;
 
 
 
 (** associated values **)
 
 (* inlined file content *)
 
 fun file_source (file: file) =
   let
     val text = cat_lines (#lines file);
     val end_pos = Position.symbol_explode text (#pos file);
   in Input.source true text (Position.range (#pos file, end_pos)) end;
 
 fun get_files (Token (_, _, Value (SOME (Files files)))) = files
   | get_files _ = [];
 
 fun put_files [] tok = tok
   | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
   | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok));
 
 
 (* document output *)
 
 fun get_output (Token (_, _, Value (SOME (Output output)))) = output
   | get_output _ = NONE;
 
 fun put_output output (Token (x, y, Slot)) = Token (x, y, Value (SOME (Output (SOME output))))
   | put_output _ tok = raise Fail ("Cannot put document output here" ^ Position.here (pos_of tok));
 
 
 (* access values *)
 
 fun get_value (Token (_, _, Value v)) = v
   | get_value _ = NONE;
 
 fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
   | map_value _ tok = tok;
 
 
 (* reports of value *)
 
 fun get_assignable_value (Token (_, _, Assignable r)) = ! r
   | get_assignable_value (Token (_, _, Value v)) = v
   | get_assignable_value _ = NONE;
 
 fun reports_of_value tok =
   (case get_assignable_value tok of
     SOME (Literal markup) =>
       let
         val pos = pos_of tok;
         val x = content_of tok;
       in
         if Position.is_reported pos then
           map (pair pos) (keyword_markup markup x :: Completion.suppress_abbrevs x)
         else []
       end
   | _ => []);
 
 
 (* name value *)
 
 fun name_value a = Name (a, Morphism.identity);
 
 fun get_name tok =
   (case get_assignable_value tok of
     SOME (Name (a, _)) => SOME a
   | _ => NONE);
 
 
 (* maxidx *)
 
 fun declare_maxidx tok =
   (case get_value tok of
     SOME (Source src) => fold declare_maxidx 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);
 
 
 (* fact values *)
 
 fun map_facts f =
   map_value (fn v =>
     (case v of
       Source src => Source (map (map_facts f) src)
     | Fact (a, ths) => Fact (a, f a ths)
     | _ => v));
 
 val trim_context_src = (map o map_facts) (K (map Thm.trim_context));
 
 
 (* transform *)
 
 fun transform phi =
   map_value (fn v =>
     (case v of
       Source src => Source (map (transform phi) src)
     | Literal _ => v
     | Name (a, psi) => Name (a, psi $> phi)
     | Typ T => Typ (Morphism.typ phi T)
     | Term t => Term (Morphism.term phi t)
     | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
     | Attribute att => Attribute (Morphism.transform phi att)
     | Declaration decl => Declaration (Morphism.transform phi decl)
     | Files _ => v
     | Output _ => v));
 
 
 (* static binding *)
 
 (*1st stage: initialize assignable slots*)
 fun init_assignable tok =
   (case tok of
     Token (x, y, Slot) => Token (x, y, Assignable (Unsynchronized.ref NONE))
   | Token (_, _, Value _) => tok
   | Token (_, _, Assignable r) => (r := NONE; tok));
 
 (*2nd stage: assign values as side-effect of scanning*)
 fun assign v tok =
   (case tok of
     Token (x, y, Slot) => Token (x, y, Value v)
   | Token (_, _, Value _) => tok
   | Token (_, _, Assignable r) => (r := v; tok));
 
 fun evaluate mk eval arg =
   let val x = eval arg in (assign (SOME (mk x)) arg; x) end;
 
 (*3rd stage: static closure of final values*)
 fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
   | closure tok = tok;
 
 
 (* pretty *)
 
 fun pretty_value ctxt tok =
   (case get_value tok of
     SOME (Literal markup) =>
       let val x = content_of tok
       in Pretty.mark_str (keyword_markup markup x, x) end
   | SOME (Name ({print, ...}, _)) => Pretty.quote (Pretty.mark_str (print ctxt))
   | SOME (Typ T) => Syntax.pretty_typ ctxt T
   | SOME (Term t) => Syntax.pretty_term ctxt t
   | SOME (Fact (_, ths)) =>
       Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
   | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
 
 
 (* src *)
 
 fun dest_src ([]: src) = raise Fail "Empty token source"
   | dest_src (head :: args) = (head, args);
 
 fun name_of_src src =
   let
     val head = #1 (dest_src src);
     val name =
       (case get_name head of
         SOME {name, ...} => name
       | NONE => content_of head);
   in (name, pos_of head) end;
 
 val args_of_src = #2 o dest_src;
 
 fun pretty_src ctxt src =
   let
     val (head, args) = dest_src src;
     val prt_name =
       (case get_name head of
         SOME {print, ...} => Pretty.mark_str (print ctxt)
       | NONE => Pretty.str (content_of head));
   in Pretty.block (Pretty.breaks (Pretty.quote prt_name :: map (pretty_value ctxt) args)) end;
 
 fun checked_src (head :: _) = is_some (get_name head)
   | checked_src [] = true;
 
 fun check_src ctxt get_table src =
   let
     val (head, args) = dest_src src;
     val table = get_table ctxt;
   in
     (case get_name head of
       SOME {name, ...} => (src, Name_Space.get table name)
     | NONE =>
         let
           val pos = pos_of head;
           val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos);
           val _ = Context_Position.report ctxt pos Markup.operator;
           val kind = Name_Space.kind_of (Name_Space.space_of_table table);
           fun print ctxt' =
             Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name;
           val value = name_value {name = name, kind = kind, print = print};
           val head' = closure (assign (SOME value) head);
         in (head' :: args, x) end)
   end;
 
 
 
 (** scanners **)
 
 open Basic_Symbol_Pos;
 
 val err_prefix = "Outer lexical error: ";
 
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 
 (* scan symbolic idents *)
 
 val scan_symid =
   Scan.many1 (Symbol.is_symbolic_char o Symbol_Pos.symbol) ||
   Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
 
 fun is_symid str =
   (case try Symbol.explode str of
     SOME [s] => Symbol.is_symbolic s orelse Symbol.is_symbolic_char s
   | SOME ss => forall Symbol.is_symbolic_char ss
   | _ => false);
 
 fun ident_or_symbolic "begin" = false
   | ident_or_symbolic ":" = true
   | ident_or_symbolic "::" = true
   | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s;
 
 
 (* scan cartouche *)
 
 val scan_cartouche =
   Symbol_Pos.scan_pos --
     ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
 
 
 (* scan space *)
 
 fun space_symbol (s, _) = Symbol.is_blank s andalso s <> "\n";
 
 val scan_space =
   Scan.many1 space_symbol @@@ Scan.optional ($$$ "\n") [] ||
   Scan.many space_symbol @@@ $$$ "\n";
 
 
 (* scan comment *)
 
 val scan_comment =
   Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body err_prefix -- Symbol_Pos.scan_pos);
 
 
 
 (** token sources **)
 
 local
 
 fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
 
 fun token k ss =
   Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.content ss), Slot);
 
 fun token_range k (pos1, (ss, pos2)) =
   Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot);
 
 fun scan_token keywords = !!! "bad input"
   (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
     scan_comment >> token_range (Comment NONE) ||
     Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
     scan_cartouche >> token_range Cartouche ||
     Antiquote.scan_control err_prefix >> (fn control =>
       token (Control control) (Antiquote.control_symbols control)) ||
     scan_space >> token Space ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
         (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
       (Lexicon.scan_longid >> pair Long_Ident ||
         Lexicon.scan_id >> pair Ident ||
         Lexicon.scan_var >> pair Var ||
         Lexicon.scan_tid >> pair Type_Ident ||
         Lexicon.scan_tvar >> pair Type_Var ||
         Symbol_Pos.scan_float >> pair Float ||
         Symbol_Pos.scan_nat >> pair Nat ||
         scan_symid >> pair Sym_Ident) >> uncurry token));
 
 fun recover msg =
   (Symbol_Pos.recover_string_qq ||
     Symbol_Pos.recover_string_bq ||
     Symbol_Pos.recover_cartouche ||
     Symbol_Pos.recover_comment ||
     Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
   >> (single o token (Error msg));
 
 in
 
 fun make_source keywords {strict} =
   let
     val scan_strict = Scan.bulk (scan_token keywords);
     val scan = if strict then scan_strict else Scan.recover scan_strict recover;
   in Source.source Symbol_Pos.stopper scan end;
 
 fun read_cartouche syms =
   (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of
     SOME tok => tok
   | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms))));
 
 end;
 
 
 (* explode *)
 
 fun tokenize keywords strict syms =
   Source.of_list syms |> make_source keywords strict |> Source.exhaust;
 
 fun explode keywords pos text =
   Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false};
 
 fun explode0 keywords = explode keywords Position.none;
 
 
 (* print names in parsable form *)
 
 fun print_name keywords name =
   ((case explode keywords Position.none name of
     [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok))
   | _ => true) ? Symbol_Pos.quote_string_qq) name;
 
 fun print_properties keywords =
   map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]";
 
 
 (* make *)
 
 fun make ((k, n), s) pos =
   let
     val pos' = Position.shift_offsets {remove_id = false} n pos;
     val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then
-        Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
+        Token ((s, range), (Vector.nth immediate_kinds k, s), Slot)
       else
         (case explode Keyword.empty_keywords pos s of
           [tok] => tok
         | _ => Token ((s, range), (Error (err_prefix ^ "exactly one token expected"), s), Slot))
   in (tok, pos') end;
 
 fun make_string (s, pos) =
   let
     val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none);
     val pos' = Position.no_range_position pos;
   in Token ((x, (pos', pos')), y, z) end;
 
 val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int;
 
 fun make_src a args = make_string a :: args;
 
 
 
 (** parsers **)
 
 type 'a parser = T list -> 'a * T list;
 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
 
 (* wrapped syntax *)
 
 fun syntax_generic scan src context =
   let
     val (name, pos) = name_of_src src;
     val old_reports = maps reports_of_value src;
     val args1 = map init_assignable (args_of_src src);
     fun reported_text () =
       if Context_Position.reports_enabled_generic context then
         let val new_reports = maps (reports_of_value o closure) args1 in
           if old_reports <> new_reports then
             map (fn (p, m) => Position.reported_text p m "") new_reports
           else []
         end
       else [];
   in
     (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
       (SOME x, (context', [])) =>
         let val _ = Output.report (reported_text ())
         in (x, context') end
     | (_, (context', args2)) =>
         let
           val print_name =
             (case get_name (hd src) of
               NONE => quote name
             | SOME {kind, print, ...} =>
                 let
                   val ctxt' = Context.proof_of context';
                   val (markup, xname) = print ctxt';
                 in plain_words kind ^ " " ^ quote (Markup.markup markup xname) end);
           val print_args =
             if null args2 then "" else ":\n  " ^ space_implode " " (map print args2);
         in
           error ("Bad arguments for " ^ print_name ^ Position.here pos ^ print_args ^
             Markup.markup_report (implode (reported_text ())))
         end)
   end;
 
 fun syntax scan src = apsnd Context.the_proof o syntax_generic scan src o Context.Proof;
 
 end;
 
 type 'a parser = 'a Token.parser;
 type 'a context_parser = 'a Token.context_parser;
diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML
+++ b/src/Pure/ROOT.ML
@@ -1,369 +1,370 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
 
 Main entry point for the Isabelle/Pure bootstrap process.
 
 Note: When this file is open in the Prover IDE, the ML files of
 Isabelle/Pure can be explored interactively. This is a separate copy of
 Pure within Pure: it does not affect the running logic session.
 *)
 
 chapter "Isabelle/Pure bootstrap";
 
 ML_file "ML/ml_name_space.ML";
 
 
 section "Bootstrap phase 0: Poly/ML setup";
 
 ML_file "ML/ml_init.ML";
 ML_file "ML/ml_system.ML";
 
 ML_file "General/basics.ML";
+ML_file "General/vector.ML";
 ML_file "General/symbol_explode.ML";
 
 ML_file "Concurrent/multithreading.ML";
 ML_file "Concurrent/unsynchronized.ML";
 ML_file "Concurrent/synchronized.ML";
 ML_file "Concurrent/counter.ML";
 
 ML_file "ML/ml_heap.ML";
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
 
 
 section "Bootstrap phase 1: towards ML within position context";
 
 subsection "Library of general tools";
 
 ML_file "library.ML";
 ML_file "General/print_mode.ML";
 ML_file "General/integer.ML";
 ML_file "General/alist.ML";
 ML_file "General/table.ML";
 ML_file "General/set.ML";
 
 ML_file "General/random.ML";
 ML_file "General/value.ML";
 ML_file "General/properties.ML";
 ML_file "General/output.ML";
 ML_file "PIDE/markup.ML";
 ML_file "General/utf8.ML";
 ML_file "General/scan.ML";
 ML_file "General/source.ML";
 ML_file "General/symbol.ML";
 ML_file "General/position.ML";
 ML_file "General/symbol_pos.ML";
 ML_file "General/input.ML";
 ML_file "General/comment.ML";
 ML_file "General/antiquote.ML";
 ML_file "ML/ml_lex.ML";
 ML_file "ML/ml_compiler1.ML";
 
 
 section "Bootstrap phase 2: towards ML within Isar context";
 
 subsection "Library of general tools";
 
 ML_file "General/stack.ML";
 ML_file "General/queue.ML";
 ML_file "General/heap.ML";
 ML_file "General/same.ML";
 ML_file "General/ord_list.ML";
 ML_file "General/balanced_tree.ML";
 ML_file "General/linear_set.ML";
 ML_file "General/change_table.ML";
 ML_file "General/buffer.ML";
 ML_file "General/pretty.ML";
 ML_file "General/rat.ML";
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";
 ML_file "System/bash.ML";
 ML_file "General/file_stream.ML";
 ML_file "General/bytes.ML";
 ML_file "General/file.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";
 ML_file "General/seq.ML";
 ML_file "General/time.ML";
 ML_file "General/timing.ML";
 ML_file "General/sha1.ML";
 
 ML_file "PIDE/yxml.ML";
 ML_file "ML/ml_profiling.ML";
 ML_file "PIDE/byte_message.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document_id.ML";
 ML_file "General/socket_io.ML";
 
 ML_file "General/graph.ML";
 
 ML_file "System/options.ML";
 
 
 subsection "Fundamental structures";
 
 ML_file "name.ML";
 ML_file "term.ML";
 ML_file "context.ML";
 ML_file "config.ML";
 ML_file "context_position.ML";
 ML_file "soft_type_system.ML";
 
 
 subsection "Concurrency within the ML runtime";
 
 ML_file "ML/exn_properties.ML";
 ML_file_no_debug "ML/exn_debugger.ML";
 
 ML_file "Concurrent/thread_data_virtual.ML";
 ML_file "Concurrent/isabelle_thread.ML";
 ML_file "Concurrent/single_assignment.ML";
 
 ML_file "Concurrent/par_exn.ML";
 ML_file "Concurrent/task_queue.ML";
 ML_file "Concurrent/future.ML";
 ML_file "Concurrent/event_timer.ML";
 ML_file "Concurrent/timeout.ML";
 ML_file "Concurrent/lazy.ML";
 ML_file "Concurrent/par_list.ML";
 
 ML_file "Concurrent/mailbox.ML";
 ML_file "Concurrent/cache.ML";
 
 ML_file "PIDE/active.ML";
 ML_file "Thy/export.ML";
 
 
 subsection "Inner syntax";
 
 ML_file "Syntax/type_annotation.ML";
 ML_file "Syntax/term_position.ML";
 ML_file "Syntax/lexicon.ML";
 ML_file "Syntax/ast.ML";
 ML_file "Syntax/syntax_ext.ML";
 ML_file "Syntax/parser.ML";
 ML_file "Syntax/syntax_trans.ML";
 ML_file "Syntax/mixfix.ML";
 ML_file "Syntax/printer.ML";
 ML_file "Syntax/syntax.ML";
 
 
 subsection "Core of tactical proof system";
 
 ML_file "term_ord.ML";
 ML_file "term_items.ML";
 ML_file "term_subst.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
 ML_file "sorts.ML";
 ML_file "type.ML";
 ML_file "logic.ML";
 ML_file "Syntax/simple_syntax.ML";
 ML_file "net.ML";
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
 ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
 ML_file "term_sharing.ML";
 ML_file "pattern.ML";
 ML_file "unify.ML";
 ML_file "theory.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
 ML_file "cterm_items.ML";
 ML_file "more_pattern.ML";
 ML_file "more_unify.ML";
 ML_file "more_thm.ML";
 
 ML_file "facts.ML";
 ML_file "thm_name.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
 ML_file "drule.ML";
 ML_file "morphism.ML";
 ML_file "variable.ML";
 ML_file "conv.ML";
 ML_file "goal_display.ML";
 ML_file "tactical.ML";
 ML_file "search.ML";
 ML_file "tactic.ML";
 ML_file "raw_simplifier.ML";
 ML_file "conjunction.ML";
 ML_file "assumption.ML";
 
 
 subsection "Isar -- Intelligible Semi-Automated Reasoning";
 
 (*ML support and global execution*)
 ML_file "ML/ml_syntax.ML";
 ML_file "ML/ml_env.ML";
 ML_file "ML/ml_options.ML";
 ML_file "ML/ml_print_depth.ML";
 ML_file_no_debug "Isar/runtime.ML";
 ML_file "PIDE/execution.ML";
 ML_file "ML/ml_compiler.ML";
 
 ML_file "skip_proof.ML";
 ML_file "goal.ML";
 
 (*outer syntax*)
 ML_file "Isar/keyword.ML";
 ML_file "Isar/token.ML";
 ML_file "Isar/parse.ML";
 ML_file "Thy/document_source.ML";
 ML_file "Thy/thy_header.ML";
 ML_file "Thy/document_marker.ML";
 
 (*proof context*)
 ML_file "Isar/object_logic.ML";
 ML_file "Isar/rule_cases.ML";
 ML_file "Isar/auto_bind.ML";
 ML_file "type_infer.ML";
 ML_file "Syntax/local_syntax.ML";
 ML_file "Isar/proof_context.ML";
 ML_file "type_infer_context.ML";
 ML_file "Syntax/syntax_phases.ML";
 ML_file "Isar/args.ML";
 
 (*theory specifications*)
 ML_file "Isar/local_defs.ML";
 ML_file "Isar/local_theory.ML";
 ML_file "Isar/entity.ML";
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_element.ML";
 ML_file "Thy/markdown.ML";
 ML_file "Thy/latex.ML";
 
 (*ML with context and antiquotations*)
 ML_file "ML/ml_context.ML";
 ML_file "ML/ml_antiquotation.ML";
 ML_file "ML/ml_compiler2.ML";
 ML_file "ML/ml_antiquotations.ML";
 
 
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
 
 (*basic proof engine*)
 ML_file "par_tactical.ML";
 ML_file "context_tactic.ML";
 ML_file "Isar/attrib.ML";
 ML_file "Isar/proof_display.ML";
 ML_file "Isar/context_rules.ML";
 ML_file "Isar/method.ML";
 ML_file "Isar/proof.ML";
 ML_file "Isar/element.ML";
 ML_file "Isar/obtain.ML";
 ML_file "Isar/subgoal.ML";
 ML_file "Isar/calculation.ML";
 
 (*local theories and targets*)
 ML_file "Isar/locale.ML";
 ML_file "Isar/generic_target.ML";
 ML_file "Isar/bundle.ML";
 ML_file "Isar/overloading.ML";
 ML_file "axclass.ML";
 ML_file "Isar/class.ML";
 ML_file "Isar/named_target.ML";
 ML_file "Isar/expression.ML";
 ML_file "Isar/interpretation.ML";
 ML_file "Isar/class_declaration.ML";
 ML_file "Isar/target_context.ML";
 ML_file "Isar/experiment.ML";
 ML_file "simplifier.ML";
 ML_file "Tools/plugin.ML";
 
 (*executable theory content*)
 ML_file "Isar/code.ML";
 
 (*specifications*)
 ML_file "Isar/spec_rules.ML";
 ML_file "Isar/specification.ML";
 ML_file "Isar/parse_spec.ML";
 ML_file "Isar/typedecl.ML";
 
 (*toplevel transactions*)
 ML_file "Isar/proof_node.ML";
 ML_file "Isar/toplevel.ML";
 
 (*proof term operations*)
 ML_file "Proof/proof_rewrite_rules.ML";
 ML_file "Proof/proof_syntax.ML";
 ML_file "Proof/proof_checker.ML";
 ML_file "Proof/extraction.ML";
 
 (*Isabelle system*)
 ML_file "PIDE/protocol_command.ML";
 ML_file "System/java.ML";
 ML_file "System/scala.ML";
 ML_file "System/process_result.ML";
 ML_file "System/isabelle_system.ML";
 
 
 (*theory documents*)
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
 ML_file "Thy/document_antiquotation.ML";
 ML_file "Thy/document_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
 ML_file "pure_syn.ML";
 ML_file "PIDE/resources.ML";
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "thm_deps.ML";
 ML_file "Thy/export_theory.ML";
 ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/document.ML";
 
 (*ML add-ons*)
 ML_file "ML/ml_pp.ML";
 ML_file "ML/ml_thms.ML";
 ML_file "ML/ml_instantiate.ML";
 ML_file "ML/ml_file.ML";
 ML_file "ML/ml_pid.ML";
 
 (*theory and proof operations*)
 ML_file "Isar/isar_cmd.ML";
 
 
 subsection "Isabelle/Isar system";
 
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
 ML_file "System/scala_compiler.ML";
 ML_file "System/isabelle_tool.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
 
 
 subsection "Miscellaneous tools and packages for Pure Isabelle";
 
 ML_file "General/base64.ML";
 ML_file "General/xz.ML";
 ML_file "General/zstd.ML";
 ML_file "Tools/prismjs.ML";
 ML_file "Tools/build.ML";
 ML_file "Tools/named_thms.ML";
 ML_file "Tools/print_operation.ML";
 ML_file "Tools/rail.ML";
 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thy_deps.ML";
 ML_file "Tools/class_deps.ML";
 ML_file "Tools/find_theorems.ML";
 ML_file "Tools/find_consts.ML";
 ML_file "Tools/simplifier_trace.ML";
 ML_file_no_debug "Tools/debugger.ML";
 ML_file "Tools/named_theorems.ML";
 ML_file "Tools/doc.ML";
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";
diff --git a/src/Pure/Syntax/lexicon.ML b/src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML
+++ b/src/Pure/Syntax/lexicon.ML
@@ -1,496 +1,496 @@
 (*  Title:      Pure/Syntax/lexicon.ML
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Lexer for the inner Isabelle syntax (terms and types).
 *)
 
 signature LEXICON =
 sig
   structure Syntax:
   sig
     val const: string -> term
     val free: string -> term
     val var: indexname -> term
   end
   val scan_id: Symbol_Pos.T list scanner
   val scan_longid: Symbol_Pos.T list scanner
   val scan_tid: Symbol_Pos.T list scanner
   val scan_hex: Symbol_Pos.T list scanner
   val scan_bin: Symbol_Pos.T list scanner
   val scan_var: Symbol_Pos.T list scanner
   val scan_tvar: Symbol_Pos.T list scanner
   val is_tid: string -> bool
   datatype token_kind =
     Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
     String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF
   eqtype token
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
   val end_pos_of_token: token -> Position.T
   val is_proper: token -> bool
   val dummy: token
   val literal: string -> token
   val is_literal: token -> bool
   val tokens_match_ord: token ord
   val mk_eof: Position.T -> token
   val eof: token
   val is_eof: token -> bool
   val stopper: token Scan.stopper
   val terminals: string list
   val is_terminal: string -> bool
   val get_terminal: string -> token option
   val suppress_literal_markup: string -> bool
   val suppress_markup: token -> bool
   val literal_markup: string -> Markup.T list
   val reports_of_token: token -> Position.report list
   val reported_token_range: Proof.context -> token -> string
   val valued_token: token -> bool
   val implode_string: Symbol.symbol list -> string
   val explode_string: string * Position.T -> Symbol_Pos.T list
   val implode_str: Symbol.symbol list -> string
   val explode_str: string * Position.T -> Symbol_Pos.T list
   val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
   val read_indexname: string -> indexname
   val read_var: string -> term
   val read_variable: string -> indexname option
   val read_nat: string -> int option
   val read_int: string -> int option
   val read_num: string -> {radix: int, leading_zeros: int, value: int}
   val read_float: string -> {mant: int, exp: int}
   val mark_class: string -> string val unmark_class: string -> string
   val mark_type: string -> string val unmark_type: string -> string
   val mark_const: string -> string val unmark_const: string -> string
   val mark_fixed: string -> string val unmark_fixed: string -> string
   val unmark:
    {case_class: string -> 'a,
     case_type: string -> 'a,
     case_const: string -> 'a,
     case_fixed: string -> 'a,
     case_default: string -> 'a} -> string -> 'a
   val is_marked: string -> bool
   val dummy_type: term
   val fun_type: term
 end;
 
 structure Lexicon: LEXICON =
 struct
 
 (** syntactic terms **)
 
 structure Syntax =
 struct
 
 fun const c = Const (c, dummyT);
 fun free x = Free (x, dummyT);
 fun var xi = Var (xi, dummyT);
 
 end;
 
 
 
 (** basic scanners **)
 
 open Basic_Symbol_Pos;
 
 val err_prefix = "Inner lexical error: ";
 
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 val scan_id = Symbol_Pos.scan_ident;
 val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id);
 val scan_tid = $$$ "'" @@@ scan_id;
 
 val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
 val scan_num = scan_hex || scan_bin || Symbol_Pos.scan_nat;
 
 val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ Symbol_Pos.scan_nat) [];
 val scan_var = $$$ "?" @@@ scan_id_nat;
 val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
 
 fun is_tid s =
   (case try (unprefix "'") s of
     SOME s' => Symbol_Pos.is_identifier s'
   | NONE => false);
 
 
 
 (** tokens **)
 
 (* datatype token_kind *)
 
 datatype token_kind =
   Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
   String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF;
 
 val token_kinds =
   Vector.fromList
    [Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str,
     String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
     Comment Comment.Latex, Dummy, EOF];
 
-fun token_kind i = Vector.sub (token_kinds, i);
+val token_kind = Vector.nth token_kinds;
 fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
 
 
 (* datatype token *)
 
 datatype token = Token of int * string * Position.range;
 
 fun index_of_token (Token (i, _, _)) = i;
 val kind_of_token = index_of_token #> token_kind;
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;
 fun end_pos_of_token (Token (_, _, (_, end_pos))) = end_pos;
 
 val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
 val dummy = Token (token_kind_index Dummy, "", Position.no_range);
 
 
 (* literals *)
 
 val literal_index = token_kind_index Literal;
 fun literal s = Token (literal_index, s, Position.no_range);
 fun is_literal tok = index_of_token tok = literal_index;
 
 fun tokens_match_ord toks =
   let val is = apply2 index_of_token toks in
     (case int_ord is of
       EQUAL => if #1 is = literal_index then fast_string_ord (apply2 str_of_token toks) else EQUAL
     | ord => ord)
   end;
 
 
 (* stopper *)
 
 val eof_index = token_kind_index EOF;
 fun mk_eof pos = Token (eof_index, "", (pos, Position.none));
 val eof = mk_eof Position.none;
 
 fun is_eof tok = index_of_token tok = eof_index;
 val stopper = Scan.stopper (K eof) is_eof;
 
 
 (* terminal symbols *)
 
 val terminal_symbols =
   [("id", Ident),
    ("longid", Long_Ident),
    ("var", Var),
    ("tid", Type_Ident),
    ("tvar", Type_Var),
    ("num_token", Num),
    ("float_token", Float),
    ("str_token", Str),
    ("string_token", String),
    ("cartouche", Cartouche)]
   |> map (apsnd token_kind_index)
   |> Symtab.make;
 
 val terminals = Symtab.keys terminal_symbols;
 val is_terminal = Symtab.defined terminal_symbols;
 fun get_terminal s =
   (case Symtab.lookup terminal_symbols s of
     SOME i => SOME (Token (i, s, Position.no_range))
   | NONE => NONE);
 
 
 (* markup *)
 
 val suppress_literal_markup = Symbol.has_control_block o Symbol.explode;
 fun suppress_markup tok = is_literal tok andalso suppress_literal_markup (str_of_token tok);
 
 fun literal_markup s =
   let val syms = Symbol.explode s in
     if Symbol.has_control_block syms then []
     else if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter syms
     then [Markup.literal]
     else [Markup.delimiter]
   end;
 
 val token_kind_markup =
  fn Type_Ident => [Markup.tfree]
   | Type_Var => [Markup.tvar]
   | Num => [Markup.numeral]
   | Float => [Markup.numeral]
   | Str => [Markup.inner_string]
   | String => [Markup.inner_string]
   | Cartouche => [Markup.inner_cartouche]
   | Comment _ => [Markup.comment1]
   | _ => [];
 
 fun reports_of_token tok =
   let
     val pos = pos_of_token tok;
     val markups =
       if is_literal tok then literal_markup (str_of_token tok)
       else token_kind_markup (kind_of_token tok);
   in map (pair pos) markups end;
 
 fun reported_token_range ctxt tok =
   if is_proper tok
   then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
   else "";
 
 
 (* valued_token *)
 
 fun valued_token tok =
   not (is_literal tok orelse is_eof tok);
 
 
 
 (** string literals **)
 
 fun explode_literal scan_body (str, pos) =
   (case Scan.read Symbol_Pos.stopper scan_body (Symbol_Pos.explode (str, pos)) of
     SOME ss => ss
   | _ => error (err_prefix ^ "malformed string literal " ^ quote str ^ Position.here pos));
 
 
 (* string *)
 
 val scan_string = Scan.trace (Symbol_Pos.scan_string_qq err_prefix) >> #2;
 val scan_string_body = Symbol_Pos.scan_string_qq err_prefix >> (#1 o #2);
 
 fun implode_string ss = quote (implode (map (fn "\"" => "\\\"" | s => s) ss));
 val explode_string = explode_literal scan_string_body;
 
 
 (* str *)
 
 val scan_chr =
   $$ "\\" |-- $$$ "'" ||
   Scan.one
     ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) o
       Symbol_Pos.symbol) >> single ||
   $$$ "'" --| Scan.ahead (~$$ "'");
 
 val scan_str =
   Scan.ahead ($$ "'" -- $$ "'") |--
     !!! "unclosed string literal"
       ($$$ "'" @@@ $$$ "'" @@@ Scan.repeats scan_chr @@@ $$$ "'" @@@ $$$ "'");
 
 val scan_str_body =
   Scan.ahead ($$ "'" |-- $$ "'") |--
     !!! "unclosed string literal"
       ($$ "'" |-- $$ "'" |-- Scan.repeats scan_chr --| $$ "'" --| $$ "'");
 
 fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss));
 val explode_str = explode_literal scan_str_body;
 
 
 
 (** tokenize **)
 
 val token_leq = op <= o apply2 str_of_token;
 
 fun token kind =
   let val i = token_kind_index kind
   in fn ss => Token (i, Symbol_Pos.content ss, Symbol_Pos.range ss) end;
 
 fun tokenize lex xids syms =
   let
     val scan_xid =
       (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
       $$$ "_" @@@ $$$ "_";
 
     val scan_val =
       scan_tvar >> token Type_Var ||
       scan_var >> token Var ||
       scan_tid >> token Type_Ident ||
       Symbol_Pos.scan_float >> token Float ||
       scan_num >> token Num ||
       scan_longid >> token Long_Ident ||
       scan_xid >> token Ident;
 
     val scan_lit = Scan.literal lex >> token Literal;
 
     val scan =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
       Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token String ||
       scan_str >> token Str ||
       Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
   in
     (case Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan)) syms of
       (toks, []) => toks
     | (_, ss) =>
         error ("Inner lexical error" ^ Position.here (#1 (Symbol_Pos.range ss)) ^
           Markup.markup Markup.no_report ("\nat " ^ quote (Symbol_Pos.content ss))))
   end;
 
 
 
 (** scan variables **)
 
 (* scan_indexname *)
 
 local
 
 val scan_vname =
   let
     fun nat n [] = n
       | nat n (c :: cs) = nat (n * 10 + (ord c - Char.ord #"0")) cs;
 
     fun idxname cs ds = (implode (rev cs), nat 0 ds);
     fun chop_idx [] ds = idxname [] ds
       | chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds
       | chop_idx (c :: cs) ds =
           if Symbol.is_digit c then chop_idx cs (c :: ds)
           else idxname (c :: cs) ds;
 
     val scan =
       (scan_id >> map Symbol_Pos.symbol) --
       Scan.optional ($$ "." |-- Symbol_Pos.scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
   in
     scan >>
       (fn (cs, ~1) => chop_idx (rev cs) []
         | (cs, i) => (implode cs, i))
   end;
 
 in
 
 val scan_indexname = $$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname;
 
 end;
 
 
 (* indexname *)
 
 fun read_indexname s =
   (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode0 s) of
     SOME xi => xi
   | _ => error ("Lexical error in variable name: " ^ quote s));
 
 
 (* read_var *)
 
 fun read_var str =
   let
     val scan =
       $$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof)
         >> Syntax.var ||
       Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
         >> (Syntax.free o implode o map Symbol_Pos.symbol);
   in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str)) end;
 
 
 (* read_variable *)
 
 fun read_variable str =
   let val scan = $$ "?" |-- scan_indexname || scan_indexname
   in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str) end;
 
 
 (* read numbers *)
 
 local
 
 fun nat cs =
   Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
     (Scan.read Symbol_Pos.stopper Symbol_Pos.scan_nat cs);
 
 in
 
 fun read_nat s = nat (Symbol_Pos.explode0 s);
 
 fun read_int s =
   (case Symbol_Pos.explode0 s of
     ("-", _) :: cs => Option.map ~ (nat cs)
   | cs => nat cs);
 
 end;
 
 
 (* read_num: hex/bin/decimal *)
 
 local
 
 val ten = Char.ord #"0" + 10;
 val a = Char.ord #"a";
 val A = Char.ord #"A";
 val _ = a > A orelse raise Fail "Bad ASCII";
 
 fun remap_hex c =
   let val x = ord c in
     if x >= a then chr (x - a + ten)
     else if x >= A then chr (x - A + ten)
     else c
   end;
 
 fun leading_zeros ["0"] = 0
   | leading_zeros ("0" :: cs) = 1 + leading_zeros cs
   | leading_zeros _ = 0;
 
 in
 
 fun read_num str =
   let
     val (radix, digs) =
       (case Symbol.explode str of
         "0" :: "x" :: cs => (16, map remap_hex cs)
       | "0" :: "b" :: cs => (2, cs)
       | cs => (10, cs));
   in
    {radix = radix,
     leading_zeros = leading_zeros digs,
     value = #1 (Library.read_radix_int radix digs)}
   end;
 
 end;
 
 fun read_float str =
   let
     val cs = Symbol.explode str;
     val (intpart, fracpart) =
       (case chop_prefix Symbol.is_digit cs of
         (intpart, "." :: fracpart) => (intpart, fracpart)
       | _ => raise Fail "read_float");
   in
    {mant = #1 (Library.read_int (intpart @ fracpart)),
     exp = length fracpart}
   end;
 
 
 (* marked logical entities *)
 
 fun marker s = (prefix s, unprefix s);
 
 val (mark_class, unmark_class) = marker "\<^class>";
 val (mark_type, unmark_type) = marker "\<^type>";
 val (mark_const, unmark_const) = marker "\<^const>";
 val (mark_fixed, unmark_fixed) = marker "\<^fixed>";
 
 fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
   (case try unmark_class s of
     SOME c => case_class c
   | NONE =>
       (case try unmark_type s of
         SOME c => case_type c
       | NONE =>
           (case try unmark_const s of
             SOME c => case_const c
           | NONE =>
               (case try unmark_fixed s of
                 SOME c => case_fixed c
               | NONE => case_default s))));
 
 val is_marked =
   unmark {case_class = K true, case_type = K true, case_const = K true,
     case_fixed = K true, case_default = K false};
 
 val dummy_type = Syntax.const (mark_type "dummy");
 val fun_type = Syntax.const (mark_type "fun");
 
 
 (* toplevel pretty printing *)
 
 val _ =
   ML_system_pp (fn _ => fn _ =>
     Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
 
 end;
diff --git a/src/Pure/Syntax/parser.ML b/src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML
+++ b/src/Pure/Syntax/parser.ML
@@ -1,714 +1,714 @@
 (*  Title:      Pure/Syntax/parser.ML
     Author:     Carsten Clasohm, Sonia Mahjoub
     Author:     Makarius
 
 General context-free parser for the inner syntax of terms and types.
 *)
 
 signature PARSER =
 sig
   type gram
   val empty_gram: gram
   val extend_gram: Syntax_Ext.xprod list -> gram -> gram
   val make_gram: Syntax_Ext.xprod list -> gram
   val pretty_gram: gram -> Pretty.T list
   datatype parsetree =
     Node of string * parsetree list |
     Tip of Lexicon.token
   exception PARSETREE of parsetree
   val pretty_parsetree: parsetree -> Pretty.T
   val parse: gram -> string -> Lexicon.token list -> parsetree list
   val branching_level: int Config.T
 end;
 
 structure Parser: PARSER =
 struct
 
 (** datatype gram **)
 
 (* nonterminals *)
 
 (*production for the NTs are stored in a vector, indexed by the NT tag*)
 type nt = int;
 
 type tags = nt Symtab.table;
 val tags_empty: tags = Symtab.empty;
 fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
 fun tags_lookup (tags: tags) = Symtab.lookup tags;
 fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
 fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
 
 type nts = Intset.T;
 val nts_empty: nts = Intset.empty;
 val nts_merge: nts * nts -> nts = Intset.merge;
 fun nts_insert nt : nts -> nts = Intset.insert nt;
 fun nts_member (nts: nts) = Intset.member nts;
 fun nts_fold f (nts: nts) = Intset.fold f nts;
 fun nts_subset (nts1: nts, nts2: nts) = Intset.forall (nts_member nts2) nts1;
 fun nts_is_empty (nts: nts) = Intset.is_empty nts;
 fun nts_is_unique (nts: nts) = Intset.size nts <= 1;
 
 
 (* tokens *)
 
 structure Tokens = Set(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);
 
 fun tokens_find P tokens = Tokens.get_first (fn tok => if P tok then SOME tok else NONE) tokens;
 fun tokens_add (nt: nt, tokens) = if Tokens.is_empty tokens then I else cons (nt, tokens);
 
 
 (* productions *)
 
 datatype symb =
   Terminal of Lexicon.token |
   Nonterminal of nt * int;  (*(tag, prio)*)
 
 structure Prods = Table(Tokens.Key);
 type prods = (symb list * string * int) list Prods.table;  (*start_token ~> [(rhs, name, prio)]*)
 
 val prods_empty: prods = Prods.empty;
 fun prods_lookup (prods: prods) = Prods.lookup_list prods;
 fun prods_update entry : prods -> prods = Prods.update entry;
 fun prods_content (prods: prods) = distinct (op =) (maps #2 (Prods.dest prods));
 
 type nt_gram = (nts * Tokens.T) * prods; (*dependent_nts, start_tokens, prods*)
   (*depent_nts is a set of all NTs whose lookahead depends on this NT's lookahead*)
 
 val nt_gram_empty: nt_gram = ((nts_empty, Tokens.empty), prods_empty);
 
 type chains = unit Int_Graph.T;
 fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains;
 fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains;
 fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains;
 val chains_empty: chains = Int_Graph.empty;
 fun chains_member (chains: chains) = Int_Graph.is_edge chains;
 fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ());
 fun chains_insert (from, to) =
   chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to);
 
 datatype gram =
   Gram of
    {nt_count: int,
     prod_count: int,
     tags: tags,
     chains: chains,
     lambdas: nts,
     prods: nt_gram Vector.vector};
     (*"tags" is used to map NT names (i.e. strings) to tags;
      chain productions are not stored as normal productions
      but instead as an entry in "chains": from -> to;
      lambda productions are stored as normal productions
      and also as an entry in "lambdas"*)
 
 (*productions for which no starting token is
   known yet are associated with this token*)
 val unknown_start = Lexicon.eof;
 
 fun get_start tks =
   (case Tokens.min tks of
     SOME tk => tk
   | NONE => unknown_start);
 
 fun add_production prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) =
   let
     (*store chain if it does not already exist*)
     val (chain, new_chain, chains') =
       (case (pri, rhs) of
         (~1, [Nonterminal (from, ~1)]) =>
           if chains_member chains (from, lhs)
           then (SOME from, false, chains)
           else (SOME from, true, chains_insert (from, lhs) chains)
       | _ =>
         let
           val chains' = chains
             |> chains_declare lhs
             |> fold (fn Nonterminal (nt, _) => chains_declare nt | _ => I) rhs;
         in (NONE, false, chains') end);
 
     (*propagate new chain in lookahead and lambdas;
       added_starts is used later to associate existing
       productions with new starting tokens*)
     val (added_starts, lambdas') =
       if not new_chain then ([], lambdas)
       else
         let (*lookahead of chain's source*)
           val ((_, from_tks), _) = Array.sub (prods, the chain);
 
           (*copy from's lookahead to chain's destinations*)
           fun copy_lookahead to =
             let
               val ((to_nts, to_tks), ps) = Array.sub (prods, to);
 
               val new_tks = Tokens.subtract to_tks from_tks;  (*added lookahead tokens*)
               val to_tks' = Tokens.merge (to_tks, new_tks);
               val _ = Array.update (prods, to, ((to_nts, to_tks'), ps));
             in tokens_add (to, new_tks) end;
 
           val tos = chains_all_succs chains' [lhs];
         in
           (fold copy_lookahead tos [],
             lambdas |> nts_member lambdas lhs ? fold nts_insert tos)
         end;
 
     (*test if new production can produce lambda
       (rhs must either be empty or only consist of lambda NTs)*)
     val new_lambdas =
       if forall
         (fn Nonterminal (id, _) => nts_member lambdas' id
           | Terminal _ => false) rhs
       then SOME (filter_out (nts_member lambdas') (chains_all_succs chains' [lhs]))
       else NONE;
     val lambdas'' = fold nts_insert (these new_lambdas) lambdas';
 
     (*list optional terminal and all nonterminals on which the lookahead
       of a production depends*)
     fun lookahead_dependency _ [] nts = (NONE, nts)
       | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts)
       | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts =
           if nts_member lambdas nt then
             lookahead_dependency lambdas symbs (nts_insert nt nts)
           else (NONE, nts_insert nt nts);
 
     (*get all known starting tokens for a nonterminal*)
     fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
 
     (*update prods, lookaheads, and lambdas according to new lambda NTs*)
     val (added_starts', lambdas') =
       let
         (*propagate added lambda NT*)
         fun propagate_lambda [] added_starts lambdas = (added_starts, lambdas)
           | propagate_lambda (l :: ls) added_starts lambdas =
               let
                 (*get lookahead for lambda NT*)
                 val ((dependent, l_starts), _) = Array.sub (prods, l);
 
                 (*check productions whose lookahead may depend on lambda NT*)
                 fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods =
                       (add_lambda, nt_dependencies, added_tks, nt_prods)
                   | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda
                         nt_dependencies added_tks nt_prods =
                       let val (tk, nts) = lookahead_dependency lambdas rhs nts_empty in
                         if nts_member nts l then       (*update production's lookahead*)
                           let
                             val new_lambda =
                               is_none tk andalso nts_subset (nts, lambdas);
 
                             val new_tks =
                               Tokens.empty
                               |> fold Tokens.insert (the_list tk)
                               |> nts_fold (curry Tokens.merge o starts_for_nt) nts
                               |> Tokens.subtract l_starts;
 
                             val added_tks' = Tokens.merge (added_tks, new_tks);
 
                             val nt_dependencies' = nts_merge (nt_dependencies, nts);
 
                             (*associate production with new starting tokens*)
                             fun copy tk nt_prods =
                               prods_update (tk, p :: prods_lookup nt_prods tk) nt_prods;
 
                             val nt_prods' = nt_prods
                               |> Tokens.fold copy new_tks
                               |> new_lambda ? copy Lexicon.dummy;
                           in
                             examine_prods ps (add_lambda orelse new_lambda)
                               nt_dependencies' added_tks' nt_prods'
                           end
                         else (*skip production*)
                           examine_prods ps add_lambda nt_dependencies added_tks nt_prods
                       end;
 
                 (*check each NT whose lookahead depends on new lambda NT*)
                 fun process_nts nt (added_lambdas, added_starts) =
                   let
                     val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
 
                     (*existing productions whose lookahead may depend on l*)
                     val tk_prods = prods_lookup nt_prods (get_start l_starts);
 
                     (*add_lambda is true if an existing production of the nt
                       produces lambda due to the new lambda NT l*)
                     val (add_lambda, nt_dependencies, added_tks, nt_prods') =
                       examine_prods tk_prods false nts_empty Tokens.empty nt_prods;
 
                     val new_nts = nts_merge (old_nts, nt_dependencies);
                     val new_tks = Tokens.merge (old_tks, added_tks);
 
                     val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
                     val _ = Array.update (prods, nt, ((new_nts, new_tks), nt_prods'));
                       (*N.B. that because the tks component
                         is used to access existing
                         productions we have to add new
                         tokens at the _end_ of the list*)
                     val added_starts' = tokens_add (nt, added_tks) added_starts;
                   in (added_lambdas', added_starts') end;
 
                 val (added_lambdas, added_starts') =
                   nts_fold process_nts dependent ([], added_starts);
                 val added_lambdas' = filter_out (nts_member lambdas) added_lambdas;
               in
                 propagate_lambda (ls @ added_lambdas') added_starts'
                   (fold nts_insert added_lambdas' lambdas)
               end;
       in
         propagate_lambda
           (nts_fold (fn l => not (nts_member lambdas l) ? cons l) lambdas'' [])
           added_starts lambdas''
       end;
 
     (*insert production into grammar*)
     val added_starts' =
       if is_some chain then added_starts'  (*don't store chain production*)
       else
         let
           (*lookahead tokens of new production and on which
             NTs lookahead depends*)
           val (start_tk, start_nts) = lookahead_dependency lambdas' rhs nts_empty;
 
           val start_tks =
             Tokens.empty
             |> fold Tokens.insert (the_list start_tk)
             |> nts_fold (curry Tokens.merge o starts_for_nt) start_nts;
 
           val start_tks' =
             start_tks
             |> (if is_some new_lambdas then Tokens.insert Lexicon.dummy
                 else if Tokens.is_empty start_tks then Tokens.insert unknown_start
                 else I);
 
           (*add lhs NT to list of dependent NTs in lookahead*)
           fun add_nts nt initial =
             (if initial then
               let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
                 if nts_member old_nts lhs then ()
                 else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps))
               end
              else (); false);
 
           (*add new start tokens to chained NTs' lookahead list;
             also store new production for lhs NT*)
           fun add_tks [] added = added
             | add_tks (nt :: nts) added =
                 let
                   val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
 
                   val new_tks = Tokens.subtract old_tks start_tks;
 
                   (*store new production*)
                   fun store tk (prods, _) =
                     let
                       val tk_prods = prods_lookup prods tk;
                       val tk_prods' = new_prod :: tk_prods;
                       val prods' = prods_update (tk, tk_prods') prods;
                     in (prods', true) end;
 
                   val (nt_prods', changed) = (nt_prods, false)
                     |> nt = lhs ? Tokens.fold store start_tks';
                   val _ =
                     if not changed andalso Tokens.is_empty new_tks then ()
                     else
                       Array.update
                         (prods, nt, ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'));
                 in add_tks nts (tokens_add (nt, new_tks) added) end;
           val _ = nts_fold add_nts start_nts true;
         in add_tks (chains_all_succs chains' [lhs]) [] end;
 
     (*associate productions with new lookaheads*)
     val _ =
       let
         (*propagate added start tokens*)
         fun add_starts [] = ()
           | add_starts ((changed_nt, new_tks) :: starts) =
               let
                 (*token under which old productions which
                   depend on changed_nt could be stored*)
                 val key =
                   tokens_find (not o Tokens.member new_tks) (starts_for_nt changed_nt)
                   |> the_default unknown_start;
 
                 (*copy productions whose lookahead depends on changed_nt;
                   if key = SOME unknown_start then tk_prods is used to hold
                   the productions not copied*)
                 fun update_prods [] result = result
                   | update_prods ((p as (rhs, _: string, _: nt)) :: ps)
                         (tk_prods, nt_prods) =
                       let
                         (*lookahead dependency for production*)
                         val (tk, depends) = lookahead_dependency lambdas' rhs nts_empty;
 
                         (*test if this production has to be copied*)
                         val update = nts_member depends changed_nt;
 
                         (*test if production could already be associated with
                           a member of new_tks*)
                         val lambda =
                           not (nts_is_unique depends) orelse
                           not (nts_is_empty depends) andalso is_some tk
                           andalso Tokens.member new_tks (the tk);
 
                         (*associate production with new starting tokens*)
                         fun copy tk nt_prods =
                           let
                             val tk_prods = prods_lookup nt_prods tk;
                             val tk_prods' =
                               if not lambda then p :: tk_prods
                               else insert (op =) p tk_prods;
                                (*if production depends on lambda NT we
                                  have to look for duplicates*)
                           in prods_update (tk, tk_prods') nt_prods end;
                         val result =
                           if update then (tk_prods, Tokens.fold copy new_tks nt_prods)
                           else if key = unknown_start then (p :: tk_prods, nt_prods)
                           else (tk_prods, nt_prods);
                       in update_prods ps result end;
 
                 (*copy existing productions for new starting tokens*)
                 fun process_nts nt =
                   let
                     val ((nts, tks), nt_prods) = Array.sub (prods, nt);
 
                     val tk_prods = prods_lookup nt_prods key;
 
                     (*associate productions with new lookahead tokens*)
                     val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods);
 
                     val nt_prods'' =
                       if key = unknown_start then
                         prods_update (key, tk_prods') nt_prods'
                       else nt_prods';
 
                     val added_tks = Tokens.subtract tks new_tks;
                     val tks' = Tokens.merge (tks, added_tks);
                     val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
                   in tokens_add (nt, added_tks) end;
 
                 val ((dependent, _), _) = Array.sub (prods, changed_nt);
               in add_starts (starts @ nts_fold process_nts dependent []) end;
       in add_starts added_starts' end;
   in (chains', lambdas') end;
 
 
 (* pretty_gram *)
 
 fun pretty_gram (Gram {tags, prods, chains, ...}) =
   let
     val print_nt = tags_name tags;
     fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ string_of_int p ^ ")");
 
     fun pretty_symb (Terminal tok) =
           if Lexicon.is_literal tok
           then Pretty.quote (Pretty.keyword1 (Lexicon.str_of_token tok))
           else Pretty.str (Lexicon.str_of_token tok)
       | pretty_symb (Nonterminal (tag, p)) = Pretty.str (print_nt tag ^ print_pri p);
 
     fun pretty_const "" = []
       | pretty_const c = [Pretty.str ("\<^bold>\<Rightarrow> " ^ quote c)];
 
     fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
 
     fun pretty_prod (name, tag) =
-      (prods_content (#2 (Vector.sub (prods, tag))) @ map prod_of_chain (chains_preds chains tag))
+      (prods_content (#2 (Vector.nth prods tag)) @ map prod_of_chain (chains_preds chains tag))
       |> map (fn (symbs, const, p) =>
           Pretty.block (Pretty.breaks
             (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const)));
   in maps pretty_prod (tags_content tags) end;
 
 
 
 (** operations on grammars **)
 
 val empty_gram =
   Gram
    {nt_count = 0,
     prod_count = 0,
     tags = tags_empty,
     chains = chains_empty,
     lambdas = nts_empty,
     prods = Vector.fromList [nt_gram_empty]};
 
 
 (*Add productions to a grammar*)
 fun extend_gram [] gram = gram
   | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
       let
         (*Get tag for existing nonterminal or create a new one*)
         fun get_tag nt_count tags nt =
           (case tags_lookup tags nt of
             SOME tag => (nt_count, tags, tag)
           | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count));
 
         (*Convert symbols to the form used by the parser;
           delimiters and predefined terms are stored as terminals,
           nonterminals are converted to integer tags*)
         fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
           | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result =
               symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result)
           | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result =
               let
                 val (nt_count', tags', new_symb) =
                   (case Lexicon.get_terminal s of
                     NONE =>
                       let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
                       in (nt_count', tags', Nonterminal (s_tag, p)) end
                   | SOME tk => (nt_count, tags, Terminal tk));
               in symb_of ss nt_count' tags' (new_symb :: result) end
           | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result;
 
         (*Convert list of productions by invoking symb_of for each of them*)
         fun prod_of [] nt_count prod_count tags result =
               (nt_count, prod_count, tags, result)
           | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
                 nt_count prod_count tags result =
               let
                 val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
                 val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' [];
               in
                 prod_of ps nt_count'' (prod_count + 1) tags''
                   ((lhs_tag, (prods, const, pri)) :: result)
               end;
 
         val (nt_count', prod_count', tags', xprods') =
           prod_of xprods nt_count prod_count tags [];
 
         (*Copy array containing productions of old grammar;
           this has to be done to preserve the old grammar while being able
           to change the array's content*)
         val prods' =
           let
             fun get_prod i =
-              if i < nt_count then Vector.sub (prods, i)
+              if i < nt_count then Vector.nth prods i
               else nt_gram_empty;
           in Array.tabulate (nt_count', get_prod) end;
 
         val (chains', lambdas') =
           (chains, lambdas) |> fold (add_production prods') xprods';
       in
         Gram
          {nt_count = nt_count',
           prod_count = prod_count',
           tags = tags',
           chains = chains',
           lambdas = lambdas',
           prods = Array.vector prods'}
       end;
 
 fun make_gram xprods = extend_gram xprods empty_gram;
 
 
 
 (** parser **)
 
 (* parsetree *)
 
 datatype parsetree =
   Node of string * parsetree list |
   Tip of Lexicon.token;
 
 exception PARSETREE of parsetree;
 
 fun pretty_parsetree parsetree =
   let
     fun pretty (Node (c, pts)) =
           [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))]
       | pretty (Tip tok) =
           if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
   in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end;
 
 
 (* parser state *)
 
 type state =
   nt * int *    (*identification and production precedence*)
   parsetree list *  (*already parsed nonterminals on rhs*)
   symb list *       (*rest of rhs*)
   string *          (*name of production*)
   int;              (*index for previous state list*)
 
 
 (*Get all rhss with precedence >= min_prec*)
 fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec);
 
 (*Get all rhss with precedence >= min_prec and < max_prec*)
 fun get_RHS' min_prec max_prec =
   filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec);
 
 (*Make states using a list of rhss*)
 fun mk_states i lhs_ID rhss =
   let fun mk_state (rhs, id, prod_prec) = (lhs_ID, prod_prec, [], rhs, id, i);
   in map mk_state rhss end;
 
 (*Add parse tree to list and eliminate duplicates
   saving the maximum precedence*)
 fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)])
   | conc (t, prec) ((t', prec') :: ts) =
       if t = t' then
         (SOME prec',
           if prec' >= prec then (t', prec') :: ts
           else (t, prec) :: ts)
       else
         let val (n, ts') = conc (t, prec) ts
         in (n, (t', prec') :: ts') end;
 
 (*Update entry in used*)
 fun update_trees (A, t) used =
   let
     val (i, ts) = the (Inttab.lookup used A);
     val (n, ts') = conc t ts;
   in (n, Inttab.update (A, (i, ts')) used) end;
 
 (*Replace entry in used*)
 fun update_prec (A, prec) =
   Inttab.map_entry A (fn (_, ts) => (prec, ts));
 
 fun getS A max_prec NONE Si =
       filter
         (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
           | _ => false) Si
   | getS A max_prec (SOME min_prec) Si =
       filter
         (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) =>
             A = B andalso prec > min_prec andalso prec <= max_prec
           | _ => false) Si;
 
 fun get_states Estate j A max_prec =
   filter
     (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
       | _ => false)
     (Array.sub (Estate, j));
 
 
 fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
   if Lexicon.valued_token c orelse id <> ""
   then (A, j, Tip c :: ts, sa, id, i)
   else (A, j, ts, sa, id, i);
 
 fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) =
   (A, j, tt @ ts, sa, id, i);
 
 fun movedot_lambda [] _ = []
   | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) =
       if k <= ki then (B, j, t @ tss, sa, id, i) :: movedot_lambda ts state
       else movedot_lambda ts state;
 
 
 (*trigger value for warnings*)
 val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)
 fun prods_for (Gram {prods, chains, ...}) tk nt =
   let
     fun token_prods prods =
       fold cons (prods_lookup prods tk) #>
       fold cons (prods_lookup prods Lexicon.dummy);
-    fun nt_prods nt = #2 (Vector.sub (prods, nt));
+    fun nt_prods nt = #2 (Vector.nth prods nt);
   in fold (token_prods o nt_prods) (chains_all_preds chains [nt]) [] end;
 
 
 fun PROCESSS gram Estate i c states =
   let
     fun processS _ [] (Si, Sii) = (Si, Sii)
       | processS used (S :: States) (Si, Sii) =
           (case S of
             (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) =>
               let (*predictor operation*)
                 val (used', new_states) =
                   (case Inttab.lookup used nt of
                     SOME (used_prec, l) => (*nonterminal has been processed*)
                       if used_prec <= min_prec then
                         (*wanted precedence has been processed*)
                         (used, movedot_lambda l S)
                       else (*wanted precedence hasn't been parsed yet*)
                         let
                           val tk_prods = prods_for gram c nt;
                           val States' =
                             mk_states i nt (get_RHS' min_prec used_prec tk_prods);
                         in (update_prec (nt, min_prec) used, movedot_lambda l S @ States') end
                   | NONE => (*nonterminal is parsed for the first time*)
                       let
                         val tk_prods = prods_for gram c nt;
                         val States' = mk_states i nt (get_RHS min_prec tk_prods);
                       in (Inttab.update (nt, (min_prec, [])) used, States') end);
               in
                 processS used' (new_states @ States) (S :: Si, Sii)
               end
           | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
               processS used States
                 (S :: Si,
                   if Lexicon.tokens_match_ord (a, c) = EQUAL then movedot_term c S :: Sii else Sii)
           | (A, prec, ts, [], id, j) => (*completer operation*)
               let val tt = if id = "" then ts else [Node (id, rev ts)] in
                 if j = i then (*lambda production?*)
                   let
                     val (prec', used') = update_trees (A, (tt, prec)) used;
                     val Slist = getS A prec prec' Si;
                     val States' = map (movedot_nonterm tt) Slist;
                   in processS used' (States' @ States) (S :: Si, Sii) end
                 else
                   let val Slist = get_states Estate j A prec
                   in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end
               end)
   in processS Inttab.empty states ([], []) end;
 
 
 fun produce gram stateset i indata prev_token =
   (case Array.sub (stateset, i) of
     [] =>
       let
         val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
         val pos = Position.here (Lexicon.pos_of_token prev_token);
       in
         if null toks then
           error ("Inner syntax error: unexpected end of input" ^ pos)
         else
           error ("Inner syntax error" ^ pos ^
             Markup.markup Markup.no_report
               ("\n" ^ Pretty.string_of
                 (Pretty.block [
                   Pretty.str "at", Pretty.brk 1,
                   Pretty.block
                    (Pretty.str "\"" ::
                     Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
                     [Pretty.str "\""])])))
       end
   | s =>
       (case indata of
         [] => s
       | c :: cs =>
           let
             val (si, sii) = PROCESSS gram stateset i c s;
             val _ = Array.update (stateset, i, si);
             val _ = Array.update (stateset, i + 1, sii);
           in produce gram stateset (i + 1) cs c end));
 
 
 fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
 
 fun earley (gram as Gram {tags, ...}) startsymbol indata =
   let
     val start_tag =
       (case tags_lookup tags startsymbol of
         SOME tag => tag
       | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol));
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);
     val _ = Array.update (Estate, 0, S0);
   in
     get_trees (produce gram Estate 0 indata Lexicon.eof)
   end;
 
 
 fun parse gram start toks =
   let
     val end_pos =
       (case try List.last toks of
         NONE => Position.none
       | SOME tok => Lexicon.end_pos_of_token tok);
     val r =
       (case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of
         [] => raise Fail "Inner syntax: no parse trees"
       | pts => pts);
   in r end;
 
 end;
diff --git a/src/Pure/library.ML b/src/Pure/library.ML
--- a/src/Pure/library.ML
+++ b/src/Pure/library.ML
@@ -1,1110 +1,1110 @@
 (*  Title:      Pure/library.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Markus Wenzel, TU Muenchen
 
 Basic library: functions, pairs, booleans, lists, integers,
 strings, lists as sets, orders, current directory, misc.
 
 See also General/basics.ML for the most fundamental concepts.
 *)
 
 infixr 0 |||
 infix 2 ?
 infix 3 o oo ooo oooo
 infix 4 ~~ upto downto
 infix orf andf
 
 signature BASIC_LIBRARY =
 sig
   (*functions*)
   val undefined: 'a -> 'b
   val I: 'a -> 'a
   val K: 'a -> 'b -> 'a
   val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   val ? : bool * ('a -> 'a) -> 'a -> 'a
   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
   val funpow: int -> ('a -> 'a) -> 'a -> 'a
   val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
 
   (*pairs*)
   val pair: 'a -> 'b -> 'a * 'b
   val rpair: 'a -> 'b -> 'b * 'a
   val fst: 'a * 'b -> 'a
   val snd: 'a * 'b -> 'b
   val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool
   val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
   val eq_pair: ('a * 'c -> bool) -> ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
   val swap: 'a * 'b -> 'b * 'a
   val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
   val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
   val apply2: ('a -> 'b) -> 'a * 'a -> 'b * 'b
 
   (*booleans*)
   val equal: ''a -> ''a -> bool
   val not_equal: ''a -> ''a -> bool
   val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool
   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
   val exists: ('a -> bool) -> 'a list -> bool
   val forall: ('a -> bool) -> 'a list -> bool
 
   (*lists*)
   val build: ('a list -> 'a list) -> 'a list
   val build_rev: ('a list -> 'a list) -> 'a list
   val single: 'a -> 'a list
   val the_single: 'a list -> 'a
   val singleton: ('a list -> 'b list) -> 'a -> 'b
   val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c
   val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option
   val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option
   val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool
   val maps: ('a -> 'b list) -> 'a list -> 'b list
   val filter: ('a -> bool) -> 'a list -> 'a list
   val filter_out: ('a -> bool) -> 'a list -> 'a list
   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
   val take: int -> 'a list -> 'a list
   val drop: int -> 'a list -> 'a list
   val chop: int -> 'a list -> 'a list * 'a list
   val chop_groups: int -> 'a list -> 'a list list
   val nth: 'a list -> int -> 'a
   val nth_list: 'a list list -> int -> 'a list
   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val nth_drop: int -> 'a list -> 'a list
   val map_index: (int * 'a -> 'b) -> 'a list -> 'b list
   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val map_range: (int -> 'a) -> int -> 'a list
   val fold_range: (int -> 'a -> 'a) -> int -> 'a -> 'a
   val split_last: 'a list -> 'a list * 'a
   val find_first: ('a -> bool) -> 'a list -> 'a option
   val find_index: ('a -> bool) -> 'a list -> int
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   val flat: 'a list list -> 'a list
   val unflat: 'a list list -> 'b list -> 'b list list
   val grouped: int -> (('a list -> 'b list) -> 'c list list -> 'd list list) ->
     ('a -> 'b) -> 'c list -> 'd list
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
   val burrow_options: ('a list -> 'b list) -> 'a option list -> 'b option list
   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
   val separate: 'a -> 'a list -> 'a list
   val surround: 'a -> 'a list -> 'a list
   val replicate: int -> 'a -> 'a list
   val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   val ~~ : 'a list * 'b list -> ('a * 'b) list
   val split_list: ('a * 'b) list -> 'a list * 'b list
   val burrow_fst: ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
   val take_prefix: ('a -> bool) -> 'a list -> 'a list
   val drop_prefix: ('a -> bool) -> 'a list -> 'a list
   val chop_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val take_suffix: ('a -> bool) -> 'a list -> 'a list
   val drop_suffix: ('a -> bool) -> 'a list -> 'a list
   val chop_suffix: ('a -> bool) -> 'a list -> 'a list * 'a list
   val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
   val chop_common_prefix: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list * ('a list * 'b list)
   val prefixes1: 'a list -> 'a list list
   val prefixes: 'a list -> 'a list list
   val suffixes1: 'a list -> 'a list list
   val suffixes: 'a list -> 'a list list
   val trim: ('a -> bool) -> 'a list -> 'a list
 
   (*integers*)
   val upto: int * int -> int list
   val downto: int * int -> int list
   val hex_digit: int -> string
   val radixpand: int * int -> int list
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
   val signed_string_of_int: int -> string
   val string_of_indexname: string * int -> string
   val read_radix_int: int -> string list -> int * string list
   val read_int: string list -> int * string list
   val oct_char: string -> string
 
   (*strings*)
   val nth_string: string -> int -> string
   val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
   val exists_string: (string -> bool) -> string -> bool
   val forall_string: (string -> bool) -> string -> bool
   val member_string: string -> string -> bool
   val last_string: string -> string option
   val first_field: string -> string -> (string * string) option
   val enclose: string -> string -> string -> string
   val unenclose: string -> string
   val quote: string -> string
   val cartouche: string -> string
   val space_implode: string -> string list -> string
   val commas: string list -> string
   val commas_quote: string list -> string
   val cat_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
   val plain_words: string -> string
   val prefix_lines: string -> string -> string
   val prefix: string -> string -> string
   val suffix: string -> string -> string
   val unprefix: string -> string -> string
   val unsuffix: string -> string -> string
   val trim_line: string -> string
   val trim_split_lines: string -> string list
   val normalize_lines: string -> string
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
   val encode_lines: string -> string
   val decode_lines: string -> string
   val align_right: string -> int -> string -> string
   val match_string: string -> string -> bool
 
   (*reals*)
   val string_of_real: real -> string
   val signed_string_of_real: real -> string
 
   (*lists as sets -- see also Pure/General/ord_list.ML*)
   val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
   val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
   val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
   val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
   val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool
   val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
   val map_transpose: ('a list -> 'b) -> 'a list list -> 'b list
 
   (*lists as multisets*)
   val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
   val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
 
   (*orders*)
   type 'a ord = 'a * 'a -> order
   val is_equal: order -> bool
   val is_less: order -> bool
   val is_less_equal: order -> bool
   val is_greater: order -> bool
   val is_greater_equal: order -> bool
   val rev_order: order -> order
   val make_ord: ('a * 'a -> bool) -> 'a ord
   val pointer_eq_ord: ('a * 'a -> order) -> 'a * 'a -> order
   val bool_ord: bool ord
   val int_ord: int ord
   val string_ord: string ord
   val size_ord: string ord
   val fast_string_ord: string ord
   val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
   val ||| : ('a -> order) * ('a -> order) -> 'a -> order
   val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
   val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   val length_ord: 'a list * 'b list -> order
   val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
   val sort: 'a ord -> 'a list -> 'a list
   val sort_distinct: 'a ord -> 'a list -> 'a list
   val sort_strings: string list -> string list
   val sort_by: ('a -> string) -> 'a list -> 'a list
   val tag_list: int -> 'a list -> (int * 'a) list
   val untag_list: (int * 'a) list -> 'a list
   val order_list: (int * 'a) list -> 'a list
 
   (*misc*)
   val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
   val divide_and_conquer': ('a -> 'b -> ('a list * ('c list * 'b -> 'c * 'b)) * 'b) ->
     'a -> 'b -> 'c * 'b
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   type serial = int
   val serial: unit -> serial
   val serial_string: unit -> string
   eqtype stamp
   val stamp: unit -> stamp
   structure Any: sig type T = exn end
   val getenv: string -> string
   val getenv_strict: string -> string
 end;
 
 signature LIBRARY =
 sig
   include BASIC_LIBRARY
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
 end;
 
 structure Library: LIBRARY =
 struct
 
 (* functions *)
 
 fun undefined _ = raise Match;
 
 fun I x = x;
 fun K x = fn _ => x;
 fun curry f x y = f (x, y);
 fun uncurry f (x, y) = f x y;
 
 (*conditional application*)
 fun b ? f = fn x => if b then f x else x;
 
 (*composition with multiple args*)
 fun (f oo g) x y = f (g x y);
 fun (f ooo g) x y z = f (g x y z);
 fun (f oooo g) x y z w = f (g x y z w);
 
 (*function exponentiation: f (... (f x) ...) with n applications of f*)
 fun funpow (0: int) _ x = x
   | funpow n f x = funpow (n - 1) f (f x);
 
 fun funpow_yield (0 : int) _ x = ([], x)
   | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
 
 
 (* pairs *)
 
 fun pair x y = (x, y);
 fun rpair x y = (y, x);
 
 fun fst (x, y) = x;
 fun snd (x, y) = y;
 
 fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2);
 fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2);
 fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2);
 
 fun swap (x, y) = (y, x);
 
 fun apfst f (x, y) = (f x, y);
 fun apsnd f (x, y) = (x, f y);
 fun apply2 f (x, y) = (f x, f y);
 
 
 (* booleans *)
 
 (*polymorphic equality*)
 fun equal x y = x = y;
 fun not_equal x y = x <> y;
 
 (*combining predicates*)
 fun p orf q = fn x => p x orelse q x;
 fun p andf q = fn x => p x andalso q x;
 
 val exists = List.exists;
 val forall = List.all;
 
 
 
 (** lists **)
 
 fun build (f: 'a list -> 'a list) = f [];
 fun build_rev f = build f |> rev;
 
 fun single x = [x];
 
 fun the_single [x] = x
   | the_single _ = raise List.Empty;
 
 fun singleton f x = the_single (f [x]);
 
 fun yield_singleton f x = f [x] #>> the_single;
 
 fun perhaps_apply funs arg =
   let
     fun app [] res = res
       | app (f :: fs) (changed, x) =
           (case f x of
             NONE => app fs (changed, x)
           | SOME x' => app fs (true, x'));
   in (case app funs (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
 
 fun perhaps_loop f arg =
   let
     fun loop (changed, x) =
       (case f x of
         NONE => (changed, x)
       | SOME x' => loop (true, x'));
   in (case loop (false, arg) of (false, _) => NONE | (true, arg') => SOME arg') end;
 
 
 (* fold -- old versions *)
 
 (*the following versions of fold are designed to fit nicely with infixes*)
 
 (*  (op @) (e, [x1, ..., xn])  ===>  ((e @ x1) @ x2) ... @ xn
     for operators that associate to the left (TAIL RECURSIVE)*)
 fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a =
   let fun itl (e, [])  = e
         | itl (e, a::l) = itl (f(e, a), l)
   in  itl end;
 
 (*  (op @) ([x1, ..., xn], e)  ===>   x1 @ (x2 ... @ (xn @ e))
     for operators that associate to the right (not tail recursive)*)
 fun foldr f (l, e) =
   let fun itr [] = e
         | itr (a::l) = f(a, itr l)
   in  itr l  end;
 
 (*  (op @) [x1, ..., xn]  ===>  ((x1 @ x2) @ x3) ... @ xn
     for operators that associate to the left (TAIL RECURSIVE)*)
 fun foldl1 f [] = raise List.Empty
   | foldl1 f (x :: xs) = foldl f (x, xs);
 
 (*  (op @) [x1, ..., xn]  ===>   x1 @ (x2 ... @ (x[n-1] @ xn))
     for n > 0, operators that associate to the right (not tail recursive)*)
 fun foldr1 f [] = raise List.Empty
   | foldr1 f l =
       let fun itr [x] = x
             | itr (x::l) = f(x, itr l)
       in  itr l  end;
 
 
 (* basic list functions *)
 
 fun eq_list eq (list1, list2) =
   pointer_eq (list1, list2) orelse
     let
       fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
         | eq_lst _ = true;
     in length list1 = length list2 andalso eq_lst (list1, list2) end;
 
 fun maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;
 
 val filter = List.filter;
 fun filter_out f = filter (not o f);
 val map_filter = List.mapPartial;
 
 fun take (0: int) xs = []
   | take _ [] = []
   | take n (x :: xs) = x :: take (n - 1) xs;
 
 fun drop (0: int) xs = xs
   | drop _ [] = []
   | drop n (x :: xs) = drop (n - 1) xs;
 
 fun chop (0: int) xs = ([], xs)
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
 fun chop_groups n list =
   (case chop (Int.max (n, 1)) list of
     ([], _) => []
   | (g, rest) => g :: chop_groups n rest);
 
 
 (*return nth element of a list, where 0 designates the first element;
   raise Subscript if list too short*)
 fun nth xs i = List.nth (xs, i);
 
 fun nth_list xss i = nth xss i handle General.Subscript => [];
 
 fun nth_map 0 f (x :: xs) = f x :: xs
   | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
   | nth_map (_: int) _ [] = raise Subscript;
 
 fun nth_drop n xs =
   List.take (xs, n) @ List.drop (xs, n + 1);
 
 fun map_index f =
   let
     fun map_aux (_: int) [] = []
       | map_aux i (x :: xs) = f (i, x) :: map_aux (i + 1) xs
   in map_aux 0 end;
 
 fun fold_index f =
   let
     fun fold_aux (_: int) [] y = y
       | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y)
   in fold_aux 0 end;
 
 fun map_range f i =
   let
     fun map_aux (k: int) =
       if k < i then f k :: map_aux (k + 1) else []
   in map_aux 0 end;
 
 fun fold_range f i =
   let
     fun fold_aux (k: int) y =
       if k < i then fold_aux (k + 1) (f k y) else y
   in fold_aux 0 end;
 
 
 (*rear decomposition*)
 fun split_last [] = raise List.Empty
   | split_last [x] = ([], x)
   | split_last (x :: xs) = apfst (cons x) (split_last xs);
 
 (*find first element satisfying predicate*)
 val find_first = List.find;
 
 (*find position of first element satisfying a predicate*)
 fun find_index pred =
   let fun find (_: int) [] = ~1
         | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   in find 0 end;
 
 (*get first element by lookup function*)
 fun get_first _ [] = NONE
   | get_first f (x :: xs) =
       (case f x of
         NONE => get_first f xs
       | some => some);
 
 fun get_index f =
   let
     fun get_aux (_: int) [] = NONE
       | get_aux i (x :: xs) =
           (case f x of
             NONE => get_aux (i + 1) xs
           | SOME y => SOME (i, y))
   in get_aux 0 end;
 
 val flat = List.concat;
 
 fun unflat (xs :: xss) ys =
       let val (ps, qs) = chop (length xs) ys
       in ps :: unflat xss qs end
   | unflat [] [] = []
   | unflat _ _ = raise ListPair.UnequalLengths;
 
 fun grouped n comb f = chop_groups n #> comb (map f) #> flat;
 
 fun burrow f xss = unflat xss (f (flat xss));
 
 fun burrow_options f os = map (try hd) (burrow f (map the_list os));
 
 fun fold_burrow f xss s =
   apfst (unflat xss) (f (flat xss) s);
 
 (*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)
 fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
   | separate _ xs = xs;
 
 fun surround s (x :: xs) = s :: x :: surround s xs
   | surround s [] = [s];
 
 (*make the list [x, x, ..., x] of length n*)
 fun replicate (n: int) x =
   let fun rep (0, xs) = xs
         | rep (n, xs) = rep (n - 1, x :: xs)
   in
     if n < 0 then raise Subscript
     else rep (n, [])
   end;
 
 
 (* direct product *)
 
 fun map_product f _ [] = []
   | map_product f [] _ = []
   | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys;
 
 fun fold_product f _ [] z = z
   | fold_product f [] _ z = z
   | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys;
 
 
 (* lists of pairs *)
 
 fun map2 _ [] [] = []
   | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
   | map2 _ _ _ = raise ListPair.UnequalLengths;
 
 fun fold2 _ [] [] z = z
   | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
   | fold2 _ _ _ _ = raise ListPair.UnequalLengths;
 
 fun map_split _ [] = ([], [])
   | map_split f (x :: xs) =
       let
         val (y, w) = f x;
         val (ys, ws) = map_split f xs;
       in (y :: ys, w :: ws) end;
 
 fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
   | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
   | zip_options _ [] = []
   | zip_options [] _ = raise ListPair.UnequalLengths;
 
 (*combine two lists forming a list of pairs:
   [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
 fun [] ~~ [] = []
   | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
   | _ ~~ _ = raise ListPair.UnequalLengths;
 
 (*inverse of ~~; the old 'split':
   [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
 val split_list = ListPair.unzip;
 
 fun burrow_fst f xs = split_list xs |>> f |> op ~~;
 
 
 (* take, drop, chop, trim according to predicate *)
 
 fun take_prefix pred list =
   let
     fun take res (x :: xs) = if pred x then take (x :: res) xs else rev res
       | take res [] = rev res;
   in take [] list end;
 
 fun drop_prefix pred list =
   let
     fun drop (x :: xs) = if pred x then drop xs else x :: xs
       | drop [] = [];
   in drop list end;
 
 fun chop_prefix pred list =
   let
     val prfx = take_prefix pred list;
     val sffx = drop (length prfx) list;
   in (prfx, sffx) end;
 
 fun take_suffix pred list =
   let
     fun take res (x :: xs) = if pred x then take (x :: res) xs else res
       | take res [] = res;
   in take [] (rev list) end;
 
 fun drop_suffix pred list =
   let
     fun drop (x :: xs) = if pred x then drop xs else rev (x :: xs)
       | drop [] = [];
   in drop (rev list) end;
 
 fun chop_suffix pred list =
   let
     val prfx = drop_suffix pred list;
     val sffx = drop (length prfx) list;
   in (prfx, sffx) end;
 
 fun trim pred = drop_prefix pred #> drop_suffix pred;
 
 
 (* prefixes, suffixes *)
 
 fun is_prefix _ [] _ = true
   | is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys
   | is_prefix eq _ _ = false;
 
 fun chop_common_prefix eq ([], ys) = ([], ([], ys))
   | chop_common_prefix eq (xs, []) = ([], (xs, []))
   | chop_common_prefix eq (xs as x :: xs', ys as y :: ys') =
       if eq (x, y) then
         let val (ps', xys'') = chop_common_prefix eq (xs', ys')
         in (x :: ps', xys'') end
       else ([], (xs, ys));
 
 fun prefixes1 [] = []
   | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
 
 fun prefixes xs = [] :: prefixes1 xs;
 
 fun suffixes1 xs = map rev (prefixes1 (rev xs));
 fun suffixes xs = [] :: suffixes1 xs;
 
 
 
 (** integers **)
 
 (* lists of integers *)
 
 (*make the list [from, from + 1, ..., to]*)
 fun ((i: int) upto j) =
   if i > j then [] else i :: (i + 1 upto j);
 
 (*make the list [from, from - 1, ..., to]*)
 fun ((i: int) downto j) =
   if i < j then [] else i :: (i - 1 downto j);
 
 
 (* convert integers to strings *)
 
 (*hexadecimal*)
 fun hex_digit i =
   if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10);
 
 (*expand the number in the given base;
   example: radixpand (2, 8) gives [1, 0, 0, 0]*)
 fun radixpand (base, num) : int list =
   let
     fun radix (n, tail) =
       if n < base then n :: tail
       else radix (n div base, (n mod base) :: tail)
   in radix (num, []) end;
 
 (*expands a number into a string of characters starting from "zerochar";
   example: radixstring (2, "0", 8) gives "1000"*)
 fun radixstring (base, zerochar, num) =
   let val offset = ord zerochar;
       fun chrof n = chr (offset + n)
   in implode (map chrof (radixpand (base, num))) end;
 
 
 local
   val zero = Char.ord #"0";
   val small_int = 10000: int;
   val small_int_table = Vector.tabulate (small_int, Int.toString);
 in
 
 fun string_of_int i =
   if i < 0 then Int.toString i
   else if i < 10 then chr (zero + i)
-  else if i < small_int then Vector.sub (small_int_table, i)
+  else if i < small_int then Vector.nth small_int_table i
   else Int.toString i;
 
 end;
 
 fun signed_string_of_int i =
   if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
 
 fun string_of_indexname (a, 0) = a
   | string_of_indexname (a, i) = a ^ "_" ^ string_of_int i;
 
 
 (* read integers *)
 
 fun read_radix_int radix cs =
   let
     val zero = Char.ord #"0";
     val limit = zero + radix;
     fun scan (num, []) = (num, [])
       | scan (num, c :: cs) =
           if zero <= ord c andalso ord c < limit then
             scan (radix * num + (ord c - zero), cs)
           else (num, c :: cs);
   in scan (0, cs) end;
 
 val read_int = read_radix_int 10;
 
 fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s)));
 
 
 
 (** strings **)
 
 (* functions tuned for strings, avoiding explode *)
 
 fun nth_string str i =
   (case try String.substring (str, i, 1) of
     SOME s => s
   | NONE => raise Subscript);
 
 fun fold_string f str x0 =
   let
     val n = size str;
     fun iter (x, i) =
       if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x;
   in iter (x0, 0) end;
 
 fun exists_string pred str =
   let
     val n = size str;
     fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1));
   in ex 0 end;
 
 fun forall_string pred = not o exists_string (not o pred);
 
 fun member_string str s = exists_string (fn s' => s = s') str;
 
 fun last_string "" = NONE
   | last_string s = SOME (str (String.sub (s, size s - 1)));
 
 fun first_field sep str =
   let
     val n = size sep;
     val len = size str;
     fun find i =
       if i + n > len then NONE
       else if String.substring (str, i, n) = sep then SOME i
       else find (i + 1);
   in
     (case find 0 of
       NONE => NONE
     | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
   end;
 
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;
 fun unenclose str = String.substring (str, 1, size str - 2);
 
 (*simple quoting (does not escape special chars)*)
 val quote = enclose "\"" "\"";
 
 val cartouche = enclose "\<open>" "\<close>";
 
 val space_implode = String.concatWith;
 
 val commas = space_implode ", ";
 val commas_quote = commas o map quote;
 
 val cat_lines = space_implode "\n";
 
 (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
 fun space_explode _ "" = []
   | space_explode sep s = String.fields (fn c => str c = sep) s;
 
 val split_lines = space_explode "\n";
 
 fun plain_words s = space_explode "_" s |> space_implode " ";
 
 fun prefix_lines "" txt = txt
   | prefix_lines prfx txt = txt |> split_lines |> map (fn s => prfx ^ s) |> cat_lines;
 
 fun prefix prfx s = prfx ^ s;
 fun suffix sffx s = s ^ sffx;
 
 fun unprefix prfx s =
   if String.isPrefix prfx s then String.substring (s, size prfx, size s - size prfx)
   else raise Fail "unprefix";
 
 fun unsuffix sffx s =
   if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
   else raise Fail "unsuffix";
 
 fun trim_line s =
   if String.isSuffix "\r\n" s
   then String.substring (s, 0, size s - 2)
   else if String.isSuffix "\r" s orelse String.isSuffix "\n" s
   then String.substring (s, 0, size s - 1)
   else s;
 
 val trim_split_lines = trim_line #> split_lines #> map trim_line;
 
 fun normalize_lines str =
   if exists_string (fn s => s = "\r") str then
     split_lines str |> map trim_line |> cat_lines
   else str;
 
 fun replicate_string (0: int) _ = ""
   | replicate_string 1 a = a
   | replicate_string k a =
       if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
       else replicate_string (k div 2) (a ^ a) ^ a;
 
 fun translate_string f = String.translate (f o String.str);
 
 val encode_lines = translate_string (fn "\n" => "\v" | c => c);
 val decode_lines = translate_string (fn "\v" => "\n" | c => c);
 
 fun align_right c k s =
   let
     val _ = if size c <> 1 orelse size s > k
       then raise Fail "align_right" else ()
   in replicate_string (k - size s) c ^ s end;
 
 (*crude matching of str against simple glob pat*)
 fun match_string pat str =
   let
     fun match [] _ = true
       | match (p :: ps) s =
           size p <= size s andalso
             (case try (unprefix p) s of
               SOME s' => match ps s'
             | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
   in match (space_explode "*" pat) str end;
 
 
 
 (** reals **)
 
 val string_of_real = Real.fmt (StringCvt.GEN NONE);
 
 fun signed_string_of_real x =
   if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
 
 
 
 (** lists as sets -- see also Pure/General/ord_list.ML **)
 
 (* canonical operations *)
 
 fun member eq list x =
   let
     fun memb [] = false
       | memb (y :: ys) = eq (x, y) orelse memb ys;
   in memb list end;
 
 fun insert eq x xs = if member eq xs x then xs else x :: xs;
 fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
 fun update eq x xs = cons x (remove eq x xs);
 
 fun inter eq xs = filter (member eq xs);
 
 fun union eq = fold (insert eq);
 fun subtract eq = fold (remove eq);
 
 fun merge eq (xs, ys) =
   if pointer_eq (xs, ys) then xs
   else if null xs then ys
   else fold_rev (insert eq) ys xs;
 
 
 (* subset and set equality *)
 
 fun subset eq (xs, ys) = forall (member eq ys) xs;
 
 fun eq_set eq (xs, ys) =
   eq_list eq (xs, ys) orelse
     (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs));
 
 
 (*makes a list of the distinct members of the input; preserves order, takes
   first of equal elements*)
 fun distinct eq lst =
   let
     fun dist (rev_seen, []) = rev rev_seen
       | dist (rev_seen, x :: xs) =
           if member eq rev_seen x then dist (rev_seen, xs)
           else dist (x :: rev_seen, xs);
   in dist ([], lst) end;
 
 (*returns a list containing all repeated elements exactly once; preserves
   order, takes first of equal elements*)
 fun duplicates eq lst =
   let
     fun dups (rev_dups, []) = rev rev_dups
       | dups (rev_dups, x :: xs) =
           if member eq rev_dups x orelse not (member eq xs x) then
             dups (rev_dups, xs)
           else dups (x :: rev_dups, xs);
   in dups ([], lst) end;
 
 fun has_duplicates eq =
   let
     fun dups [] = false
       | dups (x :: xs) = member eq xs x orelse dups xs;
   in dups end;
 
 
 (* matrices *)
 
 fun map_transpose f xss =
   let
     val n =
       (case distinct (op =) (map length xss) of
         [] => 0
       | [n] => n
       | _ => raise ListPair.UnequalLengths);
   in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
 
 
 
 (** lists as multisets **)
 
 fun remove1 eq x [] = []
   | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys;
 
 fun combine eq xs ys = fold (remove1 eq) ys xs @ ys;
 
 fun submultiset _ ([], _)  = true
   | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);
 
 
 
 (** orders **)
 
 type 'a ord = 'a * 'a -> order;
 
 fun is_equal ord = ord = EQUAL;
 fun is_less ord = ord = LESS;
 fun is_less_equal ord = ord = LESS orelse ord = EQUAL;
 fun is_greater ord = ord = GREATER;
 fun is_greater_equal ord = ord = GREATER orelse ord = EQUAL;
 
 fun rev_order LESS = GREATER
   | rev_order EQUAL = EQUAL
   | rev_order GREATER = LESS;
 
 (*compose orders*)
 fun (a_ord ||| b_ord) p = (case a_ord p of EQUAL => b_ord p | ord => ord);
 
 (*assume rel is a linear strict order*)
 fun make_ord rel (x, y) =
   if rel (x, y) then LESS
   else if rel (y, x) then GREATER
   else EQUAL;
 
 fun pointer_eq_ord ord (x, y) =
   if pointer_eq (x, y) then EQUAL else ord (x, y);
 
 fun bool_ord (false, true) = LESS
   | bool_ord (true, false) = GREATER
   | bool_ord _ = EQUAL;
 
 val int_ord = Int.compare;
 val string_ord = String.compare;
 
 val size_ord = int_ord o apply2 size;
 val fast_string_ord = pointer_eq_ord (size_ord ||| string_ord);
 
 fun option_ord ord (SOME x, SOME y) = ord (x, y)
   | option_ord _ (NONE, NONE) = EQUAL
   | option_ord _ (NONE, SOME _) = LESS
   | option_ord _ (SOME _, NONE) = GREATER;
 
 (*lexicographic product*)
 fun prod_ord a_ord b_ord ((x, y), (x', y')) =
   (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);
 
 (*dictionary order -- in general NOT well-founded!*)
 fun dict_ord elem_ord (x :: xs, y :: ys) =
       (case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys) | ord => ord)
   | dict_ord _ ([], []) = EQUAL
   | dict_ord _ ([], _ :: _) = LESS
   | dict_ord _ (_ :: _, []) = GREATER;
 
 (*lexicographic product of lists*)
 fun length_ord (xs, ys) = int_ord (length xs, length ys);
 fun list_ord elem_ord = length_ord ||| dict_ord elem_ord;
 
 
 (* sorting *)
 
 (*stable mergesort -- preserves order of equal elements*)
 fun mergesort unique ord =
   let
     fun merge (xs as x :: xs') (ys as y :: ys') =
           (case ord (x, y) of
             LESS => x :: merge xs' ys
           | EQUAL =>
               if unique then merge xs ys'
               else x :: merge xs' ys
           | GREATER => y :: merge xs ys')
       | merge [] ys = ys
       | merge xs [] = xs;
 
     fun merge_all [xs] = xs
       | merge_all xss = merge_all (merge_pairs xss)
     and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss
       | merge_pairs xss = xss;
 
     fun runs (x :: y :: xs) =
           (case ord (x, y) of
              LESS => ascending y [x] xs
            | EQUAL =>
                if unique then runs (x :: xs)
                else ascending y [x] xs
            | GREATER => descending y [x] xs)
       | runs xs = [xs]
 
     and ascending x xs (zs as y :: ys) =
           (case ord (x, y) of
              LESS => ascending y (x :: xs) ys
            | EQUAL =>
                if unique then ascending x xs ys
                else ascending y (x :: xs) ys
            | GREATER => rev (x :: xs) :: runs zs)
       | ascending x xs [] = [rev (x :: xs)]
 
     and descending x xs (zs as y :: ys) =
           (case ord (x, y) of
              GREATER => descending y (x :: xs) ys
            | EQUAL =>
                if unique then descending x xs ys
                else (x :: xs) :: runs zs
            | LESS => (x :: xs) :: runs zs)
       | descending x xs [] = [x :: xs];
 
   in merge_all o runs end;
 
 fun sort ord = mergesort false ord;
 fun sort_distinct ord = mergesort true ord;
 
 val sort_strings = sort string_ord;
 fun sort_by key xs = sort (string_ord o apply2 key) xs;
 
 
 (* items tagged by integer index *)
 
 (*insert tags*)
 fun tag_list k [] = []
   | tag_list k (x :: xs) = (k:int, x) :: tag_list (k + 1) xs;
 
 (*remove tags and suppress duplicates -- list is assumed sorted!*)
 fun untag_list [] = []
   | untag_list [(k: int, x)] = [x]
   | untag_list ((k, x) :: (rest as (k', x') :: _)) =
       if k = k' then untag_list rest
       else x :: untag_list rest;
 
 (*return list elements in original order*)
 fun order_list list = untag_list (sort (int_ord o apply2 fst) list);
 
 
 
 (** misc **)
 
 fun divide_and_conquer decomp x =
   let val (ys, recomb) = decomp x
   in recomb (map (divide_and_conquer decomp) ys) end;
 
 fun divide_and_conquer' decomp x s =
   let val ((ys, recomb), s') = decomp x s
   in recomb (fold_map (divide_and_conquer' decomp) ys s') end;
 
 
 (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
    putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)
 fun partition_list p i j =
   let
     fun part (k: int) xs =
       if k > j then
         (case xs of
           [] => []
         | _ => raise Fail "partition_list")
       else
         let val (ns, rest) = List.partition (p k) xs
         in ns :: part (k + 1) rest end;
   in part (i: int) end;
 
 fun partition_eq (eq: 'a * 'a -> bool) =
   let
     fun part [] = []
       | part (x :: ys) =
           let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
           in (x :: xs) :: part xs' end;
   in part end;
 
 
 (* serial numbers and abstract stamps *)
 
 type serial = int;
 val serial = Counter.make ();
 val serial_string = string_of_int o serial;
 
 datatype stamp = Stamp of serial;
 fun stamp () = Stamp (serial ());
 
 
 (* values of any type *)
 
 (*note that the builtin exception datatype may be extended by new
   constructors at any time*)
 structure Any = struct type T = exn end;
 
 
 (* getenv *)
 
 fun getenv x =
   (case OS.Process.getEnv x of
     NONE => ""
   | SOME y => y);
 
 fun getenv_strict x =
   (case getenv x of
     "" => error ("Undefined Isabelle environment variable: " ^ quote x)
   | y => y);
 
 end;
 
 structure Basic_Library: BASIC_LIBRARY = Library;
 open Basic_Library;
diff --git a/src/Pure/name.ML b/src/Pure/name.ML
--- a/src/Pure/name.ML
+++ b/src/Pure/name.ML
@@ -1,189 +1,189 @@
 (*  Title:      Pure/name.ML
     Author:     Makarius
 
 Names of basic logical entities (variables etc.).
 *)
 
 signature NAME =
 sig
   val uu: string
   val uu_: string
   val aT: string
   val bound: int -> string
   val is_bound: string -> bool
   val internal: string -> string
   val dest_internal: string -> string
   val is_internal: string -> bool
   val reject_internal: string * Position.T list -> unit
   val skolem: string -> string
   val dest_skolem: string -> string
   val is_skolem: string -> bool
   val reject_skolem: string * Position.T list -> unit
   val clean_index: string * int -> string * int
   val clean: string -> string
   type context
   val context: context
   val build_context: (context -> context) -> context
   val make_context: string list -> context
   val declare: string -> context -> context
   val is_declared: context -> string -> bool
   val invent: context -> string -> int -> string list
   val invent_names: context -> string -> 'a list -> (string * 'a) list
   val invent_list: string list -> string -> int -> string list
   val variant: string -> context -> string * context
   val variant_list: string list -> string list -> string list
   val enforce_case: bool -> string -> string
   val desymbolize: bool option -> string -> string
 end;
 
 structure Name: NAME =
 struct
 
 (** common defaults **)
 
 val uu = "uu";
 val uu_ = "uu_";
 val aT = "'a";
 
 
 
 (** special variable names **)
 
 (* encoded bounds *)
 
 (*names for numbered variables --
   preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*)
 
 val small_int = Vector.tabulate (1000, fn i =>
   let val leading = if i < 10 then "00" else if i < 100 then "0" else ""
   in ":" ^ leading ^ string_of_int i end);
 
 fun bound n =
-  if n < 1000 then Vector.sub (small_int, n)
-  else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
+  if n < 1000 then Vector.nth small_int n
+  else ":" ^ bound (n div 1000) ^ Vector.nth small_int (n mod 1000);
 
 val is_bound = String.isPrefix ":";
 
 
 (* internal names -- NB: internal subsumes skolem *)
 
 val internal = suffix "_";
 val dest_internal = unsuffix "_";
 val is_internal = String.isSuffix "_";
 fun reject_internal (x, ps) =
   if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
 
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
 val is_skolem = String.isSuffix "__";
 fun reject_skolem (x, ps) =
   if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
 
 fun clean_index (x, i) =
   (case try dest_internal x of
     NONE => (x, i)
   | SOME x' => clean_index (x', i + 1));
 
 fun clean x = #1 (clean_index (x, 0));
 
 
 
 (** generating fresh names **)
 
 (* context *)
 
 datatype context =
   Context of string option Symtab.table;    (*declared names with latest renaming*)
 
 fun declare x (Context tab) =
   Context (Symtab.default (clean x, NONE) tab);
 
 fun declare_renaming (x, x') (Context tab) =
   Context (Symtab.update (clean x, SOME (clean x')) tab);
 
 fun is_declared (Context tab) = Symtab.defined tab;
 fun declared (Context tab) = Symtab.lookup tab;
 
 val context = Context Symtab.empty |> fold declare ["", "'"];
 
 fun build_context (f: context -> context) = f context;
 
 val make_context = build_context o fold declare;
 
 
 (* invent names *)
 
 fun invent ctxt =
   let
     fun invs _ 0 = []
       | invs x n =
           let val x' = Symbol.bump_string x
           in if is_declared ctxt x then invs x' n else x :: invs x' (n - 1) end;
   in invs o clean end;
 
 fun invent_names ctxt x xs = invent ctxt x (length xs) ~~ xs;
 
 val invent_list = invent o make_context;
 
 
 (* variants *)
 
 (*makes a variant of a name distinct from already used names in a
   context; preserves a suffix of underscores "_"*)
 fun variant name ctxt =
   let
     fun vary x =
       (case declared ctxt x of
         NONE => x
       | SOME x' => vary (Symbol.bump_string (the_default x x')));
 
     val (x, n) = clean_index (name, 0);
     val (x', ctxt') =
       if not (is_declared ctxt x) then (x, declare x ctxt)
       else
         let
           val x0 = Symbol.bump_init x;
           val x' = vary x0;
           val ctxt' = ctxt
             |> x0 <> x' ? declare_renaming (x0, x')
             |> declare x';
         in (x', ctxt') end;
   in (x' ^ replicate_string n "_", ctxt') end;
 
 fun variant_list used names = #1 (make_context used |> fold_map variant names);
 
 
 (* names conforming to typical requirements of identifiers in the world outside *)
 
 fun enforce_case' false cs =
       (if forall Symbol.is_ascii_upper cs then map else nth_map 0) Symbol.to_ascii_lower cs
   | enforce_case' true cs =
       nth_map 0 Symbol.to_ascii_upper cs;
 
 fun enforce_case upper = implode o enforce_case' upper o raw_explode;
 
 fun desymbolize perhaps_upper "" =
       if the_default false perhaps_upper then "X" else "x"
   | desymbolize perhaps_upper s =
       let
         val xs as (x :: _) = Symbol.explode s;
         val ys =
           if Symbol.is_ascii_letter x orelse Symbol.is_symbolic x then xs
           else "x" :: xs;
         fun is_valid x =
           Symbol.is_ascii_letter x orelse Symbol.is_ascii_digit x;
         fun sep [] = []
           | sep (xs as "_" :: _) = xs
           | sep xs = "_" :: xs;
         fun desep ("_" :: xs) = xs
           | desep xs = xs;
         fun desymb x xs =
           if is_valid x then x :: xs
           else
             (case Symbol.decode x of
               Symbol.Sym name => "_" :: raw_explode name @ sep xs
             | _ => sep xs);
         val upper_lower = Option.map enforce_case' perhaps_upper |> the_default I;
       in fold_rev desymb ys [] |> desep |> upper_lower |> implode end;
 
 end;