diff --git a/src/HOL/SPARK/Tools/fdl_lexer.ML b/src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML
@@ -1,279 +1,279 @@
 (*  Title:      HOL/SPARK/Tools/fdl_lexer.ML
     Author:     Stefan Berghofer
     Copyright:  secunet Security Networks AG
 
 Lexical analyzer for fdl files.
 *)
 
 signature FDL_LEXER =
 sig
   type T
   type chars
   type banner
   type date
   type time
   datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF
   val tokenize: (chars -> 'a * chars) -> (chars -> T * chars) ->
     Position.T -> string -> 'a * T list
   val position_of: T -> Position.T
   val pos_of: T -> string
   val is_eof: T -> bool
   val stopper: T Scan.stopper
   val kind_of: T -> kind
   val content_of: T -> string
   val unparse: T -> string
   val is_proper: T -> bool
   val is_digit: string -> bool
   val c_comment: chars -> T * chars
   val curly_comment: chars -> T * chars
   val percent_comment: chars -> T * chars
   val vcg_header: chars -> (banner * (date * time) option) * chars
   val siv_header: chars ->
     (banner * (date * time) * (date * time) * (string * string)) * chars
 end;
 
 structure Fdl_Lexer: FDL_LEXER =
 struct
 
 (** tokens **)
 
 datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF;
 
 datatype T = Token of kind * string * Position.T;
 
 fun make_token k xs = Token (k, implode (map fst xs),
   case xs of [] => Position.none | (_, p) :: _ => p);
 
 fun kind_of (Token (k, _, _)) = k;
 
 fun is_proper (Token (Comment, _, _)) = false
   | is_proper _ = true;
 
 fun content_of (Token (_, s, _)) = s;
 
 fun unparse (Token (Traceability, s, _)) = "For " ^ s ^ ":"
   | unparse (Token (_, s, _)) = s;
 
 fun position_of (Token (_, _, pos)) = pos;
 
 val pos_of = Position.here o position_of;
 
 fun is_eof (Token (EOF, _, _)) = true
   | is_eof _ = false;
 
 fun mk_eof pos = Token (EOF, "", pos);
 val eof = mk_eof Position.none;
 
 val stopper =
   Scan.stopper (fn [] => eof | toks => mk_eof (position_of (List.last toks))) is_eof;
 
 fun leq_token (Token (_, s, _), Token (_, s', _)) = size s <= size s';
 
 
 (** split up a string into a list of characters (with positions) **)
 
 type chars = (string * Position.T) list;
 
 fun is_char_eof ("", _) = true
   | is_char_eof _ = false;
 
 val char_stopper = Scan.stopper (K ("", Position.none)) is_char_eof;
 
 fun symbol (x : string, _ : Position.T) = x;
 
 fun explode_pos s pos = fst (fold_map (fn x => fn pos =>
-  ((x, pos), Position.advance x pos)) (raw_explode s) pos);
+  ((x, pos), Position.advance_symbol x pos)) (raw_explode s) pos);
 
 
 (** scanners **)
 
 val any = Scan.one (not o Scan.is_stopper char_stopper);
 
 fun prfx [] = Scan.succeed []
   | prfx (x :: xs) = Scan.one (equal x o symbol) ::: prfx xs;
 
 val $$$ = prfx o raw_explode;
 
 val lexicon = Scan.make_lexicon (map raw_explode
   ["rule_family",
    "For",
    ":",
    "[",
    "]",
    "(",
    ")",
    ",",
    "&",
    ";",
    "=",
    ".",
    "..",
    "requires",
    "may_be_replaced_by",
    "may_be_deduced",
    "may_be_deduced_from",
    "are_interchangeable",
    "if",
    "end",
    "function",
    "procedure",
    "type",
    "var",
    "const",
    "array",
    "record",
    ":=",
    "of",
    "**",
    "*",
    "/",
    "div",
    "mod",
    "+",
    "-",
    "<>",
    "<",
    ">",
    "<=",
    ">=",
    "<->",
    "->",
    "not",
    "and",
    "or",
    "for_some",
    "for_all",
    "***",
    "!!!",
    "element",
    "update",
    "pending"]);
 
 fun keyword s = Scan.literal lexicon :|--
   (fn xs => if map symbol xs = raw_explode s then Scan.succeed xs else Scan.fail);
 
 fun is_digit x = "0" <= x andalso x <= "9";
 fun is_alpha x = "a" <= x andalso x <= "z" orelse "A" <= x andalso x <= "Z";
 val is_underscore = equal "_";
 val is_tilde = equal "~";
 val is_newline = equal "\n";
 val is_tab = equal "\t";
 val is_space = equal " ";
 val is_whitespace = is_space orf is_tab orf is_newline;
 val is_whitespace' = is_space orf is_tab;
 
 val number = Scan.many1 (is_digit o symbol);
 
 val identifier =
   Scan.one (is_alpha o symbol) :::
   Scan.many
     ((is_alpha orf is_digit orf is_underscore) o symbol) @@@
    Scan.optional (Scan.one (is_tilde o symbol) >> single) [];
 
 val long_identifier =
   identifier @@@ Scan.repeats1 ($$$ "." @@@ identifier);
 
 val whitespace = Scan.many (is_whitespace o symbol);
 val whitespace1 = Scan.many1 (is_whitespace o symbol);
 val whitespace' = Scan.many (is_whitespace' o symbol);
 val newline = Scan.one (is_newline o symbol);
 
 fun beginning n cs =
   let
     val drop_blanks = drop_suffix is_whitespace;
     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_whitespace c then " " else c)
       |> implode) ^ dots
   end;
 
 fun !!! text scan =
   let
     fun get_pos [] = " (end-of-input)"
       | get_pos ((_, pos) :: _) = Position.here pos;
 
     fun err (syms, msg) = fn () =>
       text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^
         (case msg of NONE => "" | SOME m => "\n" ^ m ());
   in Scan.!! err scan end;
 
 val any_line' =
   Scan.many (not o (Scan.is_stopper char_stopper orf (is_newline o symbol)));
 
 val any_line = whitespace' |-- any_line' --|
   newline >> (implode o map symbol);
 
 fun gen_comment a b = $$$ a |-- !!! "unclosed comment"
   (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment;
 
 val c_comment = gen_comment "/*" "*/";
 val curly_comment = gen_comment "{" "}";
 
 val percent_comment = $$$ "%" |-- any_line' >> make_token Comment;
 
 fun repeatn 0 _ = Scan.succeed []
   | repeatn n p = Scan.one p ::: repeatn (n-1) p;
 
 
 (** header of *.vcg and *.siv files (see simplifier/load_provenance.pro) **)
 
 type banner = string * string * string;
 type date = string * string * string;
 type time = string * string * string * string option;
 
 val asterisks = Scan.repeat1 (Scan.one (equal "*" o symbol));
 
 fun alphan n = repeatn n (is_alpha o symbol) >> (implode o map symbol);
 fun digitn n = repeatn n (is_digit o symbol) >> (implode o map symbol);
 
 val time =
   digitn 2 --| $$$ ":" -- digitn 2 --| $$$ ":" -- digitn 2 --
   Scan.option ($$$ "." |-- digitn 2) >>
     (fn (((hr, mi), s), ms) => (hr, mi, s, ms));
 
 val date =
   digitn 2 --| $$$ "-" -- alphan 3 --| $$$ "-" -- digitn 4 >>
     (fn ((d, m), y) => (d, m, y));
 
 val banner = 
   whitespace' |-- asterisks --| whitespace' --| newline :|-- (fn xs =>
     (any_line -- any_line -- any_line >>
        (fn ((l1, l2), l3) => (l1, l2, l3))) --|
     whitespace' --| prfx (map symbol xs) --| whitespace' --| newline);
 
 val vcg_header = banner -- Scan.option (whitespace |--
   $$$ "DATE :" |-- whitespace |-- date --| whitespace --|
   Scan.option ($$$ "TIME :" -- whitespace) -- time);
 
 val siv_header = banner --| whitespace --
   ($$$ "CREATED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --|
   whitespace --
   ($$$ "SIMPLIFIED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --|
   newline --| newline -- (any_line -- any_line) >>
     (fn (((b, c), s), ls) => (b, c, s, ls));
 
 
 (** the main tokenizer **)
 
 fun scan header comment =
   !!! "bad header" header --| whitespace --
   Scan.repeat (Scan.unless (Scan.one is_char_eof)
     (!!! "bad input"
        (   comment
         || (keyword "For" -- whitespace1) |--
               Scan.repeat1 (Scan.unless (keyword ":") any) --|
               keyword ":" >> make_token Traceability
         || Scan.max leq_token
              (Scan.literal lexicon >> make_token Keyword)
              (   long_identifier >> make_token Long_Ident
               || identifier >> make_token Ident)
         || number >> make_token Number) --|
      whitespace));
 
 fun tokenize header comment pos s =
   fst (Scan.finite char_stopper
     (Scan.error (scan header comment)) (explode_pos s pos));
 
 end;
diff --git a/src/Pure/General/position.ML b/src/Pure/General/position.ML
--- a/src/Pure/General/position.ML
+++ b/src/Pure/General/position.ML
@@ -1,296 +1,299 @@
 (*  Title:      Pure/General/position.ML
     Author:     Makarius
 
 Source positions starting from 1; values <= 0 mean "absent". Count Isabelle
 symbols, not UTF8 bytes nor UTF16 characters. Position range specifies a
 right-open interval offset .. end_offset (exclusive).
 *)
 
 signature POSITION =
 sig
   eqtype T
   val ord: T ord
   val make: Thread_Position.T -> T
   val dest: T -> Thread_Position.T
   val line_of: T -> int option
   val offset_of: T -> int option
   val end_offset_of: T -> int option
   val file_of: T -> string option
   val id_of: T -> string option
-  val advance: Symbol.symbol -> T -> T
+  val advance_symbol: Symbol.symbol -> T -> T
+  val advance_symbol_explode: string -> T -> T
   val advance_offsets: int -> T -> T
   val distance_of: T * T -> int option
   val none: T
   val start: T
   val file_name: string -> Properties.T
   val file_only: string -> T
   val file: string -> T
   val line_file_only: int -> string -> T
   val line_file: int -> string -> T
   val line: int -> T
   val get_props: T -> Properties.T
   val id: string -> T
   val id_only: string -> T
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
   val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
   val entity_properties_of: bool -> serial -> T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
   type report = T * Markup.T
   type report_text = report * string
   val reports_text: report_text list -> unit
   val reports: report list -> unit
   val store_reports: report_text list Unsynchronized.ref ->
     T list -> ('a -> Markup.T list) -> 'a -> unit
   val append_reports: report_text list Unsynchronized.ref -> report list -> unit
   val here_strs: T -> string * string
   val here: T -> string
   val here_list: T list -> string
   type range = T * T
   val no_range: range
   val no_range_position: T -> T
   val range_position: range -> T
   val range: T * T -> range
   val range_of_properties: Properties.T -> range
   val properties_of_range: range -> Properties.T
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
   val default: T -> bool * T
 end;
 
 structure Position: POSITION =
 struct
 
 (* datatype position *)
 
 datatype T = Pos of (int * int * int) * Properties.T;
 
 fun dest2 f = apply2 (fn Pos p => f p);
 
 val ord =
   pointer_eq_ord
    (int_ord o dest2 (#1 o #1) |||
     int_ord o dest2 (#2 o #1) |||
     int_ord o dest2 (#3 o #1) |||
     Properties.ord o dest2 #2);
 
 fun norm_props (props: Properties.T) =
   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
     [Markup.fileN, Markup.idN];
 
 fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
 fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
 
 fun valid (i: int) = i > 0;
 fun maybe_valid i = if valid i then SOME i else NONE;
 fun if_valid i i' = if valid i then i' else i;
 
 
 (* fields *)
 
 fun line_of (Pos ((i, _, _), _)) = maybe_valid i;
 fun offset_of (Pos ((_, j, _), _)) = maybe_valid j;
 fun end_offset_of (Pos ((_, _, k), _)) = maybe_valid k;
 
 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
 fun id_of (Pos (_, props)) = Properties.get props Markup.idN;
 
 
 (* advance *)
 
 fun advance_count "\n" (i: int, j: int, k: int) =
       (if_valid i (i + 1), if_valid j (j + 1), k)
   | advance_count s (i, j, k) =
       if Symbol.not_eof s then (i, if_valid j (j + 1), k)
       else (i, j, k);
 
 fun invalid_count (i, j, _: int) =
   not (valid i orelse valid j);
 
-fun advance sym (pos as (Pos (count, props))) =
+fun advance_symbol sym (pos as (Pos (count, props))) =
   if invalid_count count then pos else Pos (advance_count sym count, props);
 
+val advance_symbol_explode = fold advance_symbol o Symbol.explode;
+
 fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) =
   if offset = 0 orelse invalid_count count then pos
   else if offset < 0 then raise Fail "Illegal offset"
   else if valid i then raise Fail "Illegal line position"
   else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props);
 
 
 (* distance of adjacent positions *)
 
 fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) =
   if valid j andalso valid j' then SOME (j' - j) else NONE;
 
 
 (* make position *)
 
 val none = Pos ((0, 0, 0), []);
 val start = Pos ((1, 1, 0), []);
 
 
 fun file_name "" = []
   | file_name name = [(Markup.fileN, name)];
 
 fun file_only name = Pos ((0, 0, 0), file_name name);
 fun file name = Pos ((1, 1, 0), file_name name);
 
 fun line_file_only i name = Pos ((i, 0, 0), file_name name);
 fun line_file i name = Pos ((i, 1, 0), file_name name);
 fun line i = line_file i "";
 
 fun get_props (Pos (_, props)) = props;
 
 fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 
 fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
 fun copy_id pos = (case id_of pos of NONE => I | SOME id => put_id id);
 
 fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
 fun id_properties_of pos =
   (case id_of pos of
     SOME id => [(Markup.idN, id)]
   | NONE => []);
 
 fun adjust_offsets adjust (pos as Pos (_, props)) =
   if is_none (file_of pos) then
     (case parse_id pos of
       SOME id =>
         (case adjust id of
           SOME offset =>
             let val Pos (count, _) = advance_offsets offset pos
             in Pos (count, Properties.remove Markup.idN props) end
         | NONE => pos)
     | NONE => pos)
   else pos;
 
 
 (* markup properties *)
 
 fun get props name =
   (case Properties.get props name of
     NONE => 0
   | SOME s => Value.parse_int s);
 
 fun of_properties props =
   make {line = get props Markup.lineN,
     offset = get props Markup.offsetN,
     end_offset = get props Markup.end_offsetN,
     props = props};
 
 fun value k i = if valid i then [(k, Value.print_int i)] else [];
 
 fun properties_of (Pos ((i, j, k), props)) =
   value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
 
 fun offset_properties_of (Pos ((_, j, k), _)) =
   value Markup.offsetN j @ value Markup.end_offsetN k;
 
 val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
 
 fun entity_markup kind (name, pos) =
   Markup.entity kind name |> Markup.properties (def_properties_of pos);
 
 fun entity_properties_of def serial pos =
   if def then (Markup.defN, Value.print_int serial) :: properties_of pos
   else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
 
 val markup = Markup.properties o properties_of;
 
 
 (* reports *)
 
 fun is_reported pos = is_some (offset_of pos) andalso is_some (id_of pos);
 fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
 
 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
 fun report_text pos markup txt = Output.report [reported_text pos markup txt];
 fun report pos markup = report_text pos markup "";
 
 type report = T * Markup.T;
 type report_text = report * string;
 
 val reports_text =
   map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "")
   #> Output.report;
 
 val reports = map (rpair "") #> reports_text;
 
 fun store_reports _ [] _ _ = ()
   | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
 
 fun append_reports (r: report_text list Unsynchronized.ref) reports =
   Unsynchronized.change r (append (map (rpair "") reports));
 
 
 (* here: user output *)
 
 fun here_strs pos =
   (case (line_of pos, file_of pos) of
     (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
   | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
   | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
   | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
 
 fun here pos =
   let
     val props = properties_of pos;
     val (s1, s2) = here_strs pos;
   in
     if s2 = "" then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
 val here_list = map here #> distinct (op =) #> implode;
 
 
 (* range *)
 
 type range = T * T;
 
 val no_range = (none, none);
 
 fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
 fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
 fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
 
 fun range_of_properties props =
   let
     val pos = of_properties props;
     val pos' =
       make {line = get props Markup.end_lineN,
         offset = get props Markup.end_offsetN,
         end_offset = 0,
         props = props};
   in (pos, pos') end;
 
 fun properties_of_range (pos, pos') =
   properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos'));
 
 
 (* thread data *)
 
 val thread_data = make o Thread_Position.get;
 fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
 
 fun default pos =
   if pos = none then (false, thread_data ())
   else (true, pos);
 
 end;
diff --git a/src/Pure/General/symbol_pos.ML b/src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML
+++ b/src/Pure/General/symbol_pos.ML
@@ -1,308 +1,308 @@
 (*  Title:      Pure/General/symbol_pos.ML
     Author:     Makarius
 
 Symbols with explicit position information.
 *)
 
 signature SYMBOL_POS =
 sig
   type T = Symbol.symbol * Position.T
   type 'a scanner = T list -> 'a * T list
   val symbol: T -> Symbol.symbol
   val content: T list -> string
   val range: T list -> Position.range
   val is_eof: T -> bool
   val stopper: T Scan.stopper
   val !!! : Scan.message -> 'a scanner -> 'a scanner
   val $$ : Symbol.symbol -> T scanner
   val ~$$ : Symbol.symbol -> T scanner
   val $$$ : Symbol.symbol -> T list scanner
   val ~$$$ : Symbol.symbol -> T list scanner
   val scan_pos: Position.T scanner
   val scan_string_q: string -> (Position.T * (T list * Position.T)) scanner
   val scan_string_qq: string -> (Position.T * (T list * Position.T)) scanner
   val scan_string_bq: string -> (Position.T * (T list * Position.T)) scanner
   val recover_string_q: T list scanner
   val recover_string_qq: T list scanner
   val recover_string_bq: T list scanner
   val quote_string_q: string -> string
   val quote_string_qq: string -> string
   val quote_string_bq: string -> string
   val cartouche_content: T list -> T list
   val scan_cartouche: string -> T list scanner
   val scan_cartouche_content: string -> T list scanner
   val recover_cartouche: T list scanner
   val scan_comment: string -> T list scanner
   val scan_comment_body: string -> T list scanner
   val recover_comment: T list scanner
   val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
     (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
   type text = string
   val implode: T list -> text
   val implode_range: Position.range -> T list -> text * Position.range
   val explode_delete: text * Position.T -> T list * Position.T list
   val explode: text * Position.T -> T list
   val explode0: string -> T list
   val scan_ident: T list scanner
   val is_identifier: string -> bool
   val scan_nat: T list scanner
   val scan_float: T list scanner
 end;
 
 structure Symbol_Pos: SYMBOL_POS =
 struct
 
 (* type T *)
 
 type T = Symbol.symbol * Position.T;
 type 'a scanner = T list -> 'a * T list;
 
 fun symbol ((s, _): T) = s;
 
 val content = implode o map symbol;
 
 fun range (syms as (_, pos) :: _) =
-      let val pos' = List.last syms |-> Position.advance
+      let val pos' = List.last syms |-> Position.advance_symbol
       in Position.range (pos, pos') end
   | range [] = Position.no_range;
 
 
 (* stopper *)
 
 fun mk_eof pos = (Symbol.eof, pos);
 val eof = mk_eof Position.none;
 
 val is_eof = Symbol.is_eof o symbol;
 
 val stopper =
-  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance)) is_eof;
+  Scan.stopper (fn [] => eof | inp => mk_eof (List.last inp |-> Position.advance_symbol)) is_eof;
 
 
 (* basic scanners *)
 
 fun !!! text (scan: 'a scanner) =
   let
     fun get_pos [] = " (end-of-input)"
       | get_pos ((_, pos) :: _) = Position.here pos;
 
     fun err (syms, msg) = fn () =>
       text () ^ get_pos syms ^
       Markup.markup Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^
       (case msg of NONE => "" | SOME m => "\n" ^ m ());
   in Scan.!! err scan end;
 
 fun $$ s = Scan.one (fn x => symbol x = s);
 fun ~$$ s = Scan.one (fn x => symbol x <> s);
 
 fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
 fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
 
 val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
 
 
 (* scan string literals *)
 
 local
 
 val char_code =
   Scan.one (Symbol.is_ascii_digit o symbol) --
   Scan.one (Symbol.is_ascii_digit o symbol) --
   Scan.one (Symbol.is_ascii_digit o symbol) :|--
   (fn (((a, pos), (b, _)), (c, _)) =>
     let val (n, _) = Library.read_int [a, b, c]
     in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
 
 fun scan_str q err_prefix =
   $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string")
     ($$$ q || $$$ "\\" || char_code) ||
   Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.not_eof s) >> single;
 
 fun scan_strs q err_prefix =
   Scan.ahead ($$ q) |--
     !!! (fn () => err_prefix ^ "unclosed string literal")
       ((scan_pos --| $$$ q) -- (Scan.repeats (scan_str q err_prefix) -- ($$$ q |-- scan_pos)));
 
 fun recover_strs q =
   $$$ q @@@ Scan.repeats (Scan.permissive (scan_str q ""));
 
 in
 
 val scan_string_q = scan_strs "'";
 val scan_string_qq = scan_strs "\"";
 val scan_string_bq = scan_strs "`";
 
 val recover_string_q = recover_strs "'";
 val recover_string_qq = recover_strs "\"";
 val recover_string_bq = recover_strs "`";
 
 end;
 
 
 (* quote string literals *)
 
 local
 
 fun char_code i =
   (if i < 10 then "00" else if i < 100 then "0" else "") ^ string_of_int i;
 
 fun quote_str q s =
   if Symbol.is_ascii_control s then "\\" ^ char_code (ord s)
   else if s = q orelse s = "\\" then "\\" ^ s
   else s;
 
 fun quote_string q = enclose q q o implode o map (quote_str q) o Symbol.explode;
 
 in
 
 val quote_string_q = quote_string "'";
 val quote_string_qq = quote_string "\"";
 val quote_string_bq = quote_string "`";
 
 end;
 
 
 (* nested text cartouches *)
 
 fun cartouche_content syms =
   let
     fun err () =
       error ("Malformed text cartouche: "
         ^ quote (content syms) ^ Position.here (#1 (range syms)));
   in
     (case syms of
       ("\<open>", _) :: rest =>
         (case rev rest of
           ("\<close>", _) :: rrest => rev rrest
         | _ => err ())
     | _ => err ())
   end;
 
 val scan_cartouche_depth =
   Scan.repeat1 (Scan.depend (fn (depth: int option) =>
     (case depth of
       SOME d =>
         $$ Symbol.open_ >> pair (SOME (d + 1)) ||
           (if d > 0 then
             Scan.one (fn (s, _) => s <> Symbol.close andalso Symbol.not_eof s) >> pair depth ||
             $$ Symbol.close >> pair (if d = 1 then NONE else SOME (d - 1))
           else Scan.fail)
     | NONE => Scan.fail)));
 
 fun scan_cartouche err_prefix =
   Scan.ahead ($$ Symbol.open_) |--
     !!! (fn () => err_prefix ^ "unclosed text cartouche")
       (Scan.provide is_none (SOME 0) scan_cartouche_depth);
 
 fun scan_cartouche_content err_prefix =
   scan_cartouche err_prefix >> cartouche_content;
 
 val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
 
 
 (* ML-style comments *)
 
 local
 
 val scan_cmt =
   Scan.depend (fn (d: int) => $$$ "(" @@@ $$$ "*" >> pair (d + 1)) ||
   Scan.depend (fn 0 => Scan.fail | d => $$$ "*" @@@ $$$ ")" >> pair (d - 1)) ||
   Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
   Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
 
 val scan_cmts = Scan.pass 0 (Scan.repeats scan_cmt);
 
 in
 
 fun scan_comment err_prefix =
   Scan.ahead ($$ "(" -- $$ "*") |--
     !!! (fn () => err_prefix ^ "unclosed comment")
       ($$$ "(" @@@ $$$ "*" @@@ scan_cmts @@@ $$$ "*" @@@ $$$ ")");
 
 fun scan_comment_body err_prefix =
   Scan.ahead ($$ "(" -- $$ "*") |--
     !!! (fn () => err_prefix ^ "unclosed comment")
       ($$ "(" |-- $$ "*" |-- scan_cmts --| $$ "*" --| $$ ")");
 
 val recover_comment =
   $$$ "(" @@@ $$$ "*" @@@ scan_cmts;
 
 end;
 
 
 (* source *)
 
 fun source pos =
   Source.source' pos Symbol.stopper (Scan.bulk (Scan.depend (fn pos =>
-    Scan.one Symbol.not_eof >> (fn s => (Position.advance s pos, (s, pos))))));
+    Scan.one Symbol.not_eof >> (fn s => (Position.advance_symbol s pos, (s, pos))))));
 
 
 (* compact representation -- with Symbol.DEL padding *)
 
 type text = string;
 
 fun pad [] = []
   | pad [(s, _)] = [s]
   | pad ((s1, pos1) :: (rest as (_, pos2) :: _)) =
       let
-        val end_pos1 = Position.advance s1 pos1;
+        val end_pos1 = Position.advance_symbol s1 pos1;
         val d = Int.max (0, the_default 0 (Position.distance_of (end_pos1, pos2)));
       in s1 :: replicate d Symbol.DEL @ pad rest end;
 
 val implode = implode o pad;
 
 fun implode_range (pos1, pos2) syms =
   let val syms' = (("", pos1) :: syms @ [("", pos2)])
   in (implode syms', range syms') end;
 
 fun explode_delete (str, pos) =
   let
     val (res, _) =
-      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
+      fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance_symbol s p))
         (Symbol.explode str) ([], Position.no_range_position pos);
   in
     fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p)))
       res ([], [])
   end;
 
 val explode = explode_delete #> #1;
 fun explode0 str = explode (str, Position.none);
 
 
 (* identifiers *)
 
 local
 
 val letter = Scan.one (symbol #> Symbol.is_letter);
 val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
 
 val sub = Scan.one (symbol #> (fn s => s = "\<^sub>"));
 
 in
 
 val scan_ident = letter ::: Scan.repeats (letdigs1 || sub ::: letdigs1);
 
 end;
 
 fun is_identifier s =
   Symbol.is_ascii_identifier s orelse
     (case try (Scan.finite stopper scan_ident) (explode0 s) of
       SOME (_, []) => true
     | _ => false);
 
 
 (* numerals *)
 
 val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
 val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
 
 end;
 
 structure Basic_Symbol_Pos =   (*not open by default*)
 struct
   val $$ = Symbol_Pos.$$;
   val ~$$ = Symbol_Pos.~$$;
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;
 
 type 'a scanner = 'a Symbol_Pos.scanner;
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 | Verbatim | Cartouche | Comment of Comment.kind option |
     (*special content*)
     Error of string | EOF
   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
   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 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_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 read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a option
   val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   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 | Verbatim | Cartouche | Comment of Comment.kind option |
   (*special content*)
   Error of string | EOF;
 
 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"
   | Verbatim => "verbatim text"
   | Cartouche => "text 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
     | Verbatim => true
     | Cartouche => 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;
 
 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', _), _)) = k = k';
 
 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, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (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 delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos));
     in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete 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
   | Verbatim => enclose "{*" "*}" x
   | Cartouche => cartouche x
   | 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 = fold Position.advance (Symbol.explode text) (#pos file);
+    val end_pos = Position.advance_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));
 
 
 (* 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));
 
 
 (* 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 verbatim text *)
 
 val scan_verb =
   $$$ "*" --| Scan.ahead (~$$ "}") ||
   Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s) >> single;
 
 val scan_verbatim =
   Scan.ahead ($$ "{" -- $$ "*") |--
     !!! "unclosed verbatim text"
       ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
         (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
 
 val recover_verbatim =
   $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb;
 
 
 (* 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_verbatim >> token_range Verbatim ||
     scan_cartouche >> token_range Cartouche ||
     scan_comment >> token_range (Comment NONE) ||
     Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
     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 ||
     recover_verbatim ||
     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.advance_offsets 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)
       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);
 
 
 (* read body -- e.g. antiquotation source *)
 
 fun read_body keywords scan =
   tokenize (Keyword.no_command_keywords keywords) {strict = true}
   #> filter is_proper
   #> Scan.read stopper scan;
 
 fun read_antiq keywords scan (syms, pos) =
   (case read_body keywords scan syms of
     SOME x => x
   | NONE => error ("Malformed antiquotation" ^ Position.here pos));
 
 
 (* 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/ML/ml_lex.ML b/src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML
+++ b/src/Pure/ML/ml_lex.ML
@@ -1,394 +1,394 @@
 (*  Title:      Pure/ML/ml_lex.ML
     Author:     Makarius
 
 Lexical syntax for Isabelle/ML and Standard ML.
 *)
 
 signature ML_LEX =
 sig
   val keywords: string list
   datatype token_kind =
     Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
     Space | Comment of Comment.kind option | Error of string | EOF
   eqtype token
   val stopper: token Scan.stopper
   val is_regular: token -> bool
   val is_improper: token -> bool
   val is_comment: token -> bool
   val set_range: Position.range -> token -> token
   val range_of: token -> Position.range
   val pos_of: token -> Position.T
   val end_pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
   val check_content_of: token -> string
   val flatten: token list -> string
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
   val tokenize: string -> token list
   val tokenize_range: Position.range -> string -> token list
   val read_text: Symbol_Pos.text * Position.T -> token Antiquote.antiquote list
   val read: Symbol_Pos.text -> token Antiquote.antiquote list
   val read_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
   val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} ->
     token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
   val read_source: Input.source -> token Antiquote.antiquote list
   val read_source_sml: Input.source -> token Antiquote.antiquote list
   val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
 struct
 
 (** keywords **)
 
 val keywords =
  ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>", "[",
   "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", "case",
   "datatype", "do", "else", "end", "eqtype", "exception", "fn", "fun",
   "functor", "handle", "if", "in", "include", "infix", "infixr",
   "let", "local", "nonfix", "of", "op", "open", "orelse", "raise",
   "rec", "sharing", "sig", "signature", "struct", "structure", "then",
   "type", "val", "where", "while", "with", "withtype"];
 
 val keywords2 =
  ["and", "case", "do", "else", "end", "if", "in", "let", "local", "of",
   "sig", "struct", "then", "while", "with"];
 
 val keywords3 =
  ["handle", "open", "raise"];
 
 val lexicon = Scan.make_lexicon (map raw_explode keywords);
 
 
 
 (** tokens **)
 
 (* datatype token *)
 
 datatype token_kind =
   Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String |
   Space | Comment of Comment.kind option | Error of string | EOF;
 
 datatype token = Token of Position.range * (token_kind * string);
 
 
 (* position *)
 
 fun set_range range (Token (_, x)) = Token (range, x);
 fun range_of (Token (range, _)) = range;
 
 val pos_of = #1 o range_of;
 val end_pos_of = #2 o range_of;
 
 
 (* stopper *)
 
 fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
 val eof = mk_eof Position.none;
 
 fun is_eof (Token (_, (EOF, _))) = true
   | is_eof _ = false;
 
 val stopper =
   Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* token content *)
 
 fun kind_of (Token (_, (k, _))) = k;
 
 fun content_of (Token (_, (_, x))) = x;
 fun token_leq (tok, tok') = content_of tok <= content_of tok';
 
 fun is_keyword (Token (_, (Keyword, _))) = true
   | is_keyword _ = false;
 
 fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x)
   | is_delimiter _ = false;
 
 fun is_regular (Token (_, (Error _, _))) = false
   | is_regular (Token (_, (EOF, _))) = false
   | is_regular _ = true;
 
 fun is_improper (Token (_, (Space, _))) = true
   | is_improper (Token (_, (Comment _, _))) = true
   | is_improper _ = false;
 
 fun is_comment (Token (_, (Comment _, _))) = true
   | is_comment _ = false;
 
 fun warning_opaque tok =
   (case tok of
     Token (_, (Keyword, ":>")) =>
       warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
         \prefer non-opaque matching (:) possibly with abstype" ^
         Position.here (pos_of tok))
   | _ => ());
 
 fun check_content_of tok =
   (case kind_of tok of
     Error msg => error msg
   | _ => content_of tok);
 
 
 (* flatten *)
 
 fun flatten_content (tok :: (toks as tok' :: _)) =
       Symbol.escape (check_content_of tok) ::
         (if is_improper tok orelse is_improper tok' then flatten_content toks
          else Symbol.space :: flatten_content toks)
   | flatten_content toks = map (Symbol.escape o check_content_of) toks;
 
 val flatten = implode o flatten_content;
 
 
 (* markup *)
 
 local
 
 val token_kind_markup =
  fn Type_Var => (Markup.ML_tvar, "")
   | Word => (Markup.ML_numeral, "")
   | Int => (Markup.ML_numeral, "")
   | Real => (Markup.ML_numeral, "")
   | Char => (Markup.ML_char, "")
   | String => (Markup.ML_string, "")
   | Comment _ => (Markup.ML_comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 in
 
 fun token_report (tok as Token ((pos, _), (kind, x))) =
   let
     val (markup, txt) =
       if not (is_keyword tok) then token_kind_markup kind
       else if is_delimiter tok then (Markup.ML_delimiter, "")
       else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "")
       else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "")
       else (Markup.ML_keyword1 |> Markup.keyword_properties, "");
   in ((pos, markup), txt) end;
 
 end;
 
 
 
 (** scanners **)
 
 open Basic_Symbol_Pos;
 
 val err_prefix = "SML lexical error: ";
 
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 
 (* identifiers *)
 
 local
 
 val scan_letdigs =
   Scan.many (Symbol.is_ascii_letdig o Symbol_Pos.symbol);
 
 val scan_alphanumeric =
   Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) ::: scan_letdigs;
 
 val scan_symbolic =
   Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
 
 in
 
 val scan_ident = scan_alphanumeric || scan_symbolic;
 
 val scan_long_ident =
   Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "=");
 
 val scan_type_var = $$$ "'" @@@ scan_letdigs;
 
 end;
 
 
 (* numerals *)
 
 local
 
 val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol);
 val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_sign = Scan.optional ($$$ "~") [];
 val scan_decint = scan_sign @@@ scan_dec;
 val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;
 
 in
 
 val scan_word =
   $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex ||
   $$$ "0" @@@ $$$ "w" @@@ scan_dec;
 
 val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
 
 val scan_rat = scan_decint @@@ Scan.optional ($$$ "/" @@@ scan_dec) [];
 
 val scan_real =
   scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
   scan_decint @@@ scan_exp;
 
 end;
 
 
 (* chars and strings *)
 
 val scan_blanks1 = Scan.many1 (Symbol.is_ascii_blank o Symbol_Pos.symbol);
 
 local
 
 val scan_escape =
   Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
   $$$ "^" @@@
     (Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) ||
   Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
     Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
     Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
 
 val scan_str =
   Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso
     (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
   $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
 
 val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
 val scan_gaps = Scan.repeats scan_gap;
 
 in
 
 val scan_char =
   $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\"";
 
 val recover_char =
   $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) [];
 
 val scan_string =
   Scan.ahead ($$ "\"") |--
     !!! "unclosed string literal"
       ($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\"");
 
 val recover_string =
   $$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str);
 
 end;
 
 
 (* rat antiquotation *)
 
 val rat_name = Symbol_Pos.explode ("Pure.rat ", Position.none);
 
 val scan_rat_antiq =
   Symbol_Pos.scan_pos -- ($$ "@" |-- Symbol_Pos.scan_pos -- scan_rat) -- Symbol_Pos.scan_pos
     >> (fn ((pos1, (pos2, body)), pos3) =>
       {start = Position.range_position (pos1, pos2),
        stop = Position.none,
        range = Position.range (pos1, pos3),
        body = rat_name @ body});
 
 
 (* scan tokens *)
 
 local
 
 fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss));
 
 val scan_sml =
   scan_char >> token Char ||
   scan_string >> token String ||
   scan_blanks1 >> token Space ||
   Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
   Scan.max token_leq
    (Scan.literal lexicon >> token Keyword)
    (scan_word >> token Word ||
     scan_real >> token Real ||
     scan_int >> token Int ||
     scan_long_ident >> token Long_Ident ||
     scan_ident >> token Ident ||
     scan_type_var >> token Type_Var);
 
 val scan_sml_antiq = scan_sml >> Antiquote.Text;
 
 val scan_ml_antiq =
   Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
   Antiquote.scan_control >> Antiquote.Control ||
   Antiquote.scan_antiq >> Antiquote.Antiq ||
   scan_rat_antiq >> Antiquote.Antiq ||
   scan_sml_antiq;
 
 fun recover msg =
  (recover_char ||
   recover_string ||
   Symbol_Pos.recover_cartouche ||
   Symbol_Pos.recover_comment ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
   >> (single o token (Error msg));
 
 fun reader {opaque_warning} scan syms =
   let
     val termination =
       if null syms then []
       else
         let
-          val pos1 = List.last syms |-> Position.advance;
-          val pos2 = Position.advance Symbol.space pos1;
+          val pos1 = List.last syms |-> Position.advance_symbol;
+          val pos2 = Position.advance_symbol Symbol.space pos1;
         in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
 
     fun check (Antiquote.Text tok) =
           (check_content_of tok; if opaque_warning then warning_opaque tok else ())
       | check _ = ();
     val input =
       Source.of_list syms
       |> Source.source Symbol_Pos.stopper
         (Scan.recover (Scan.bulk (!!! "bad input" scan))
           (fn msg => recover msg >> map Antiquote.Text))
       |> Source.exhaust;
     val _ = Position.reports (Antiquote.antiq_reports input);
     val _ = Position.reports_text (maps (fn Antiquote.Text t => [token_report t] | _ => []) input);
     val _ = List.app check input;
   in input @ termination end;
 
 in
 
 fun source src =
   Symbol_Pos.source (Position.line 1) src
   |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_sml)) recover);
 
 val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust;
 fun tokenize_range range = tokenize #> map (set_range range);
 
 val read_text = reader {opaque_warning = true} scan_ml_antiq o Symbol_Pos.explode;
 fun read text = read_text (text, Position.none);
 
 fun read_range range =
   read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
 
 fun read_source' {language, symbols, opaque_warning} scan source =
   let
     val pos = Input.pos_of source;
     val _ =
       if Position.is_reported_range pos
       then Position.report pos (language (Input.is_delimited source))
       else ();
   in
     Input.source_explode source
     |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p))
     |> reader {opaque_warning = opaque_warning} scan
   end;
 
 val read_source =
   read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true}
     scan_ml_antiq;
 
 val read_source_sml =
   read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
     scan_sml_antiq;
 
 val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq;
 
 end;
 
 end;
diff --git a/src/Pure/Pure.thy b/src/Pure/Pure.thy
--- a/src/Pure/Pure.thy
+++ b/src/Pure/Pure.thy
@@ -1,1540 +1,1540 @@
 (*  Title:      Pure/Pure.thy
     Author:     Makarius
 
 The Pure theory, with definitions of Isar commands and some lemmas.
 *)
 
 theory Pure
 keywords
     "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
     "overloaded" "pervasive" "premises" "structure" "unchecked"
   and "private" "qualified" :: before_command
   and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
     "obtains" "shows" "when" "where" "|" :: quasi_command
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl
   and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations"
     "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias"
     "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
   and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn
   and "axiomatization" :: thy_stmt
   and "external_file" "bibtex_file" "ROOTS_file" :: thy_load
   and "generate_file" :: thy_decl
   and "export_generated_files" :: diag
   and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
   and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   and "ML_val" "ML_command" :: diag % "ML"
   and "simproc_setup" :: thy_decl % "ML"
   and "setup" "local_setup" "attribute_setup" "method_setup"
     "declaration" "syntax_declaration"
     "parse_ast_translation" "parse_translation" "print_translation"
     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
   and "bundle" :: thy_decl_block
   and "unbundle" :: thy_decl
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" "experiment" :: thy_decl_block
   and "interpret" :: prf_goal % "proof"
   and "interpretation" "global_interpretation" "sublocale" :: thy_goal
   and "class" :: thy_decl_block
   and "subclass" :: thy_goal
   and "instantiation" :: thy_decl_block
   and "instance" :: thy_goal
   and "overloading" :: thy_decl_block
   and "opening" :: quasi_command
   and "code_datatype" :: thy_decl
   and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt
   and "schematic_goal" :: thy_goal_stmt
   and "notepad" :: thy_decl_block
   and "have" :: prf_goal % "proof"
   and "hence" :: prf_goal % "proof"
   and "show" :: prf_asm_goal % "proof"
   and "thus" :: prf_asm_goal % "proof"
   and "then" "from" "with" :: prf_chain % "proof"
   and "note" :: prf_decl % "proof"
   and "supply" :: prf_script % "proof"
   and "using" "unfolding" :: prf_decl % "proof"
   and "fix" "assume" "presume" "define" :: prf_asm % "proof"
   and "consider" :: prf_goal % "proof"
   and "obtain" :: prf_asm_goal % "proof"
   and "guess" :: prf_script_asm_goal % "proof"
   and "let" "write" :: prf_decl % "proof"
   and "case" :: prf_asm % "proof"
   and "{" :: prf_open % "proof"
   and "}" :: prf_close % "proof"
   and "next" :: next_block % "proof"
   and "qed" :: qed_block % "proof"
   and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof"
   and "done" :: "qed_script" % "proof"
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
   and "apply_end" :: prf_script % "proof"
   and "subgoal" :: prf_script_goal % "proof"
   and "proof" :: prf_block % "proof"
   and "also" "moreover" :: prf_decl % "proof"
   and "finally" "ultimately" :: prf_chain % "proof"
   and "back" :: prf_script % "proof"
   and "help" "print_commands" "print_options" "print_context" "print_theory"
     "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
     "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings"
     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
   and "print_state" :: diag
   and "welcome" :: diag
   and "end" :: thy_end
   and "realizers" :: thy_decl
   and "realizability" :: thy_decl
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
 abbrevs "\\tag" = "\<^marker>\<open>tag \<close>"
   and "===>" = "===>"  (*prevent replacement of very long arrows*)
   and "--->" = "\<midarrow>\<rightarrow>"
   and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = ""
   and "hence" = "then have"
   and "thus" = "then show"
 begin
 
 section \<open>Isar commands\<close>
 
 subsection \<open>Other files\<close>
 
 ML \<open>
 local
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file"
       (Resources.provide_parse_file >> (fn get_file => Toplevel.theory (#2 o get_file)));
 
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>bibtex_file\<close> "check bibtex database file in Prover IDE"
       (Resources.provide_parse_file >> (fn get_file =>
         Toplevel.theory (fn thy =>
           let
             val ({lines, pos, ...}, thy') = get_file thy;
             val _ = Bibtex.check_database_output pos (cat_lines lines);
           in thy' end)));
 
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>ROOTS_file\<close> "session ROOTS file"
       (Resources.provide_parse_file >> (fn get_file =>
         Toplevel.theory (fn thy =>
           let
             val ({src_path, lines, pos = pos0, ...}, thy') = get_file thy;
             val ctxt = Proof_Context.init_global thy';
             val dir = Path.dir (Path.expand (Resources.master_directory thy' + src_path));
             val _ =
               (lines, pos0) |-> fold (fn line => fn pos1 =>
                 let
-                  val pos2 = pos1 |> fold Position.advance (Symbol.explode line);
+                  val pos2 = Position.advance_symbol_explode line pos1;
                   val range = Position.range (pos1, pos2);
                   val source = Input.source true line range;
                   val _ =
                     if line = "" then ()
                     else if String.isPrefix "#" line then
                       Context_Position.report ctxt (#1 range) Markup.comment
                     else
                       (ignore (Resources.check_session_dir ctxt (SOME dir) source)
                         handle ERROR msg => Output.error_message msg);
-                in pos2 |> Position.advance "\n" end);
+                in pos2 |> Position.advance_symbol "\n" end);
           in thy' end)));
 
   val _ =
     Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
       "generate source file, with antiquotations"
       (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.embedded_input)
         >> Generated_Files.generate_file_cmd);
 
 
   val files_in_theory =
     (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
       Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.theory_name --| \<^keyword>\<open>)\<close>));
 
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>export_generated_files\<close>
       "export generated files from given theories"
       (Parse.and_list1 files_in_theory >> (fn args =>
         Toplevel.keep (fn st =>
           Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args)));
 
 
   val base_dir =
     Scan.optional (\<^keyword>\<open>(\<close> |--
       Parse.!!! (\<^keyword>\<open>in\<close> |-- Parse.path_input --| \<^keyword>\<open>)\<close>)) (Input.string "");
 
   val external_files = Scan.repeat1 Parse.path_input -- base_dir;
 
   val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false;
   val executable = \<^keyword>\<open>(\<close> |-- Parse.!!! (exe --| \<^keyword>\<open>)\<close>) >> SOME || Scan.succeed NONE;
 
   val export_files = Scan.repeat1 Parse.path_binding -- executable;
 
   val _ =
     Outer_Syntax.command \<^command_keyword>\<open>compile_generated_files\<close>
       "compile generated files and export results"
       (Parse.and_list files_in_theory --
         Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) [] --
         Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
         Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("", Position.none) --
         (Parse.where_ |-- Parse.!!! Parse.ML_source)
         >> (fn ((((args, external), export), export_prefix), source) =>
           Toplevel.keep (fn st =>
             Generated_Files.compile_generated_files_cmd
               (Toplevel.context_of st) args external export export_prefix source)));
 
 in end\<close>
 
 external_file "ROOT0.ML"
 external_file "ROOT.ML"
 
 
 subsection \<open>Embedded ML text\<close>
 
 ML \<open>
 local
 
 val semi = Scan.option \<^keyword>\<open>;\<close>;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_file\<close> "read and evaluate Isabelle/ML file"
     (Resources.parse_file --| semi >> ML_File.ML NONE);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_file_debug\<close>
     "read and evaluate Isabelle/ML file (with debugger information)"
     (Resources.parse_file --| semi >> ML_File.ML (SOME true));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_file_no_debug\<close>
     "read and evaluate Isabelle/ML file (no debugger information)"
     (Resources.parse_file --| semi >> ML_File.ML (SOME false));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>SML_file\<close> "read and evaluate Standard ML file"
     (Resources.parse_file --| semi >> ML_File.SML NONE);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>SML_file_debug\<close>
     "read and evaluate Standard ML file (with debugger information)"
     (Resources.parse_file --| semi >> ML_File.SML (SOME true));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>SML_file_no_debug\<close>
     "read and evaluate Standard ML file (no debugger information)"
     (Resources.parse_file --| semi >> ML_File.SML (SOME false));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>SML_export\<close> "evaluate SML within Isabelle/ML environment"
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
           {environment = ML_Env.SML_export, redirect = false, verbose = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
       end));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>SML_import\<close> "evaluate Isabelle/ML within SML environment"
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
           {environment = ML_Env.SML_import, redirect = false, verbose = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
             Local_Theory.propagate_ml_env)
       end));
 
 val _ =
   Outer_Syntax.command ("ML_export", \<^here>)
     "ML text within theory or local theory, and export to bootstrap environment"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory (fn context =>
         context
         |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle
         |> Config.put_generic ML_Env.ML_write_global true
         |> ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
         |> Config.restore_generic ML_Env.ML_write_global context
         |> Config.restore_generic ML_Env.ML_environment context
         |> Local_Theory.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
     (Parse.ML_source >> (fn source =>
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #>
           Proof.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_val\<close> "diagnostic ML text"
     (Parse.ML_source >> Isar_Cmd.ml_diag true);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_command\<close> "diagnostic ML text (silent)"
     (Parse.ML_source >> Isar_Cmd.ml_diag false);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>setup\<close> "ML setup for global theory"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>local_setup\<close> "ML setup for local theory"
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>oracle\<close> "declare oracle"
     (Parse.range Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>attribute_setup\<close> "define attribute in ML"
     (Parse.name_position --
         Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>method_setup\<close> "define proof method in ML"
     (Parse.name_position --
         Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
       >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>declaration\<close> "generic ML declaration"
     (Parse.opt_keyword "pervasive" -- Parse.ML_source
       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>syntax_declaration\<close> "generic ML syntax declaration"
     (Parse.opt_keyword "pervasive" -- Parse.ML_source
       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
     (Parse.name_position --
       (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close> --| \<^keyword>\<open>=\<close>) --
       Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
 
 in end\<close>
 
 
 subsection \<open>Theory commands\<close>
 
 subsubsection \<open>Sorts and types\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>default_sort\<close>
     "declare default sort for explicit type variables"
     (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>typedecl\<close> "type declaration"
     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
       >> (fn ((args, a), mx) =>
           Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>type_synonym\<close> "declare type abbreviation"
     (Parse.type_args -- Parse.binding --
       (\<^keyword>\<open>=\<close> |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
       >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
 
 in end\<close>
 
 
 subsubsection \<open>Consts\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>judgment\<close> "declare object-logic judgment"
     (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>consts\<close> "declare constants"
     (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
 
 in end\<close>
 
 
 subsubsection \<open>Syntax and translations\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>nonterminal\<close>
     "declare syntactic type constructors (grammar nonterminal symbols)"
     (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
       >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
       >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
 
 val trans_pat =
   Scan.optional
     (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\<open>)\<close>)) "logic"
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
   ((\<^keyword>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>) >> K Syntax.Parse_Rule ||
     (\<^keyword>\<open>\<leftharpoondown>\<close> || \<^keyword>\<open><=\<close>) >> K Syntax.Print_Rule ||
     (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) >> K Syntax.Parse_Print_Rule) toks;
 
 val trans_line =
   trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
     >> (fn (left, (arr, right)) => arr (left, right));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>translations\<close> "add syntax translation rules"
     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
 
 in end\<close>
 
 
 subsubsection \<open>Translation functions\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>parse_ast_translation\<close>
     "install parse ast translation functions"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>parse_translation\<close>
     "install parse translation functions"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_translation\<close>
     "install print translation functions"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>typed_print_translation\<close>
     "install typed print translation functions"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_ast_translation\<close>
     "install print ast translation functions"
     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
 
 in end\<close>
 
 
 subsubsection \<open>Specifications\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.local_theory' \<^command_keyword>\<open>definition\<close> "constant definition"
     (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
       Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
         #2 oo Specification.definition_cmd decl params prems spec));
 
 val _ =
   Outer_Syntax.local_theory' \<^command_keyword>\<open>abbreviation\<close> "constant abbreviation"
     (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
       >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
 
 val axiomatization =
   Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --
   Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>axiomatization\<close> "axiomatic constant specification"
     (Scan.optional Parse.vars [] --
       Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
       >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>alias\<close> "name-space alias for constant"
     (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.name_position)
       >> Specification.alias_cmd);
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>type_alias\<close> "name-space alias for type constructor"
     (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.name_position)
       >> Specification.type_alias_cmd);
 
 in end\<close>
 
 
 subsubsection \<open>Notation\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>type_notation\<close>
     "add concrete syntax for type constructors"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>no_type_notation\<close>
     "delete concrete syntax for type constructors"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>notation\<close>
     "add concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>no_notation\<close>
     "delete concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
       >> (fn (mode, args) => Specification.notation_cmd false mode args));
 
 in end\<close>
 
 
 subsubsection \<open>Theorems\<close>
 
 ML \<open>
 local
 
 val long_keyword =
   Parse_Spec.includes >> K "" ||
   Parse_Spec.long_statement_keyword;
 
 val long_statement =
   Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
   Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
     >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
 
 val short_statement =
   Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
     >> (fn ((shows, assumes), fixes) =>
       (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
         Element.Shows shows));
 
 fun theorem spec schematic descr =
   Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
     ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) =>
       ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
         long Thm.theoremK NONE (K I) binding includes elems concl)));
 
 val _ = theorem \<^command_keyword>\<open>theorem\<close> false "theorem";
 val _ = theorem \<^command_keyword>\<open>lemma\<close> false "lemma";
 val _ = theorem \<^command_keyword>\<open>corollary\<close> false "corollary";
 val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition";
 val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal";
 
 in end\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas\<close> "define theorems"
     (Parse_Spec.name_facts -- Parse.for_fixes >>
       (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
 
 val _ =
   Outer_Syntax.local_theory' \<^command_keyword>\<open>declare\<close> "declare theorems"
     (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
       >> (fn (facts, fixes) =>
           #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>named_theorems\<close>
     "declare named collection of theorems"
     (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
       fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
 
 in end\<close>
 
 
 subsubsection \<open>Hide names\<close>
 
 ML \<open>
 local
 
 fun hide_names command_keyword what hide parse prep =
   Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
     ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
       (Toplevel.theory (fn thy =>
         let val ctxt = Proof_Context.init_global thy
         in fold (hide fully o prep ctxt) args thy end))));
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_class\<close> "classes" Sign.hide_class Parse.class
     Proof_Context.read_class;
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_type\<close> "types" Sign.hide_type Parse.type_const
     ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_const\<close> "consts" Sign.hide_const Parse.const
     ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
 
 val _ =
   hide_names \<^command_keyword>\<open>hide_fact\<close> "facts" Global_Theory.hide_fact
     Parse.name_position (Global_Theory.check_fact o Proof_Context.theory_of);
 
 in end\<close>
 
 
 subsection \<open>Bundled declarations\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>bundle\<close>
     "define bundle of declarations"
     ((Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
       >> (uncurry Bundle.bundle_cmd))
     (Parse.binding --| Parse.begin >> Bundle.init);
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
     "activate declarations from bundle in local theory"
     (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>include\<close>
     "activate declarations from bundle in proof body"
     (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>including\<close>
     "activate declarations from bundle in goal refinement"
     (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>
     "print bundles of declarations"
     (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
 
 in end\<close>
 
 
 subsection \<open>Local theory specifications\<close>
 
 subsubsection \<open>Specification context\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
     (((Parse.name_position -- Scan.optional Parse_Spec.opening [])
         >> (fn (name, incls) => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd incls name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
         >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems)))
       --| Parse.begin);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>end\<close> "end context"
     (Scan.succeed
       (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o
         Toplevel.end_proof (K Proof.end_notepad)));
 
 in end\<close>
 
 
 subsubsection \<open>Locales and interpretation\<close>
 
 ML \<open>
 local
 
 val locale_context_elements =
   Scan.repeat1 Parse_Spec.context_element;
 
 val locale_val =
   ((Parse_Spec.locale_expression -- Scan.optional Parse_Spec.opening [])
     || Parse_Spec.opening >> pair ([], []))
   -- Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! locale_context_elements) []
   || locale_context_elements >> pair (([], []), []);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>locale\<close> "define named specification context"
     (Parse.binding --
       Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) ((([], []), []), []) -- Parse.opt_begin
       >> (fn ((name, ((expr, includes), elems)), begin) =>
           Toplevel.begin_main_target begin
             (Expression.add_locale_cmd name Binding.empty includes expr elems #> snd)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>experiment\<close> "open private specification context"
     (Scan.repeat Parse_Spec.context_element --| Parse.begin
       >> (fn elems =>
           Toplevel.begin_main_target true (Experiment.experiment_cmd elems #> snd)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
     "prove interpretation of locale expression in proof context"
     (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
       Toplevel.proof (Interpretation.interpret_cmd expr)));
 
 val interpretation_args_with_defs =
   Parse.!!! Parse_Spec.locale_expression --
     (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
       -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) ([]));
 
 val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
     "prove interpretation of locale expression into global theory"
     (interpretation_args_with_defs >> (fn (expr, defs) =>
       Interpretation.global_interpretation_cmd expr defs));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.name_position --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
       interpretation_args_with_defs >> (fn (loc, (expr, defs)) =>
         Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs)))
     || interpretation_args_with_defs >> (fn (expr, defs) =>
         Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
     "prove interpretation of locale expression in local theory or into global theory"
     (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
       Toplevel.local_theory_to_proof NONE NONE
         (Interpretation.isar_interpretation_cmd expr)));
 
 in end\<close>
 
 
 subsubsection \<open>Type classes\<close>
 
 ML \<open>
 local
 
 val class_context_elements =
   Scan.repeat1 Parse_Spec.context_element;
 
 val class_val =
   ((Parse_Spec.class_expression -- Scan.optional Parse_Spec.opening [])
     || Parse_Spec.opening >> pair [])
   -- Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! class_context_elements) [] ||
   class_context_elements >> pair ([], []);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
    (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) (([], []), []) -- Parse.opt_begin
     >> (fn ((name, ((supclasses, includes), elems)), begin) =>
         Toplevel.begin_main_target begin
           (Class_Declaration.class_cmd name includes supclasses elems #> snd)));
 
 val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>subclass\<close> "prove a subclass relation"
     (Parse.class >> Class_Declaration.subclass_cmd);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>instantiation\<close> "instantiate and prove type arity"
    (Parse.multi_arity --| Parse.begin
      >> (fn arities => Toplevel.begin_main_target true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>instance\<close> "prove type arity or subclass relation"
   ((Parse.class --
     ((\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
     Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
 
 in end\<close>
 
 
 subsubsection \<open>Arbitrary overloading\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>overloading\<close> "overloaded definitions"
    (Scan.repeat1 (Parse.name --| (\<^keyword>\<open>==\<close> || \<^keyword>\<open>\<equiv>\<close>) -- Parse.term --
       Scan.optional (\<^keyword>\<open>(\<close> |-- (\<^keyword>\<open>unchecked\<close> >> K false) --| \<^keyword>\<open>)\<close>) true
       >> Scan.triple1) --| Parse.begin
    >> (fn operations => Toplevel.begin_main_target true (Overloading.overloading_cmd operations)));
 
 in end\<close>
 
 
 subsection \<open>Proof commands\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>notepad\<close> "begin proof context"
     (Parse.begin >> K Proof.begin_notepad);
 
 in end\<close>
 
 
 subsubsection \<open>Statements\<close>
 
 ML \<open>
 local
 
 val structured_statement =
   Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
     >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>have\<close> "state local goal"
     (structured_statement >> (fn (a, b, c, d) =>
       Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>show\<close> "state local goal, to refine pending subgoals"
     (structured_statement >> (fn (a, b, c, d) =>
       Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>hence\<close> "old-style alias of \"then have\""
     (structured_statement >> (fn (a, b, c, d) =>
       Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thus\<close> "old-style alias of  \"then show\""
     (structured_statement >> (fn (a, b, c, d) =>
       Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
 
 in end\<close>
 
 
 subsubsection \<open>Local facts\<close>
 
 ML \<open>
 local
 
 val facts = Parse.and_list1 Parse.thms1;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>then\<close> "forward chaining"
     (Scan.succeed (Toplevel.proof Proof.chain));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>from\<close> "forward chaining from given facts"
     (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>with\<close> "forward chaining from given and current facts"
     (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>note\<close> "define facts"
     (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>supply\<close> "define facts during goal refinement (unstructured)"
     (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>using\<close> "augment goal facts"
     (facts >> (Toplevel.proof o Proof.using_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>unfolding\<close> "unfold definitions in goal and facts"
     (facts >> (Toplevel.proof o Proof.unfolding_cmd));
 
 in end\<close>
 
 
 subsubsection \<open>Proof context\<close>
 
 ML \<open>
 local
 
 val structured_statement =
   Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
     >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>fix\<close> "fix local variables (Skolem constants)"
     (Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>assume\<close> "assume propositions"
     (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>presume\<close> "assume propositions, to be established later"
     (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>define\<close> "local definition (non-polymorphic)"
     ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
       >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>consider\<close> "state cases rule"
     (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>obtain\<close> "generalized elimination"
     (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
       >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>guess\<close> "wild guessing (unstructured)"
     (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>let\<close> "bind text variables"
     (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\<open>=\<close> |-- Parse.term))
       >> (Toplevel.proof o Proof.let_bind_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>write\<close> "add concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
     >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>case\<close> "invoke local context"
     (Parse_Spec.opt_thm_name ":" --
       (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.name_position -- Scan.repeat (Parse.maybe Parse.binding)
           --| \<^keyword>\<open>)\<close>) ||
         Parse.name_position >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
 
 in end\<close>
 
 
 subsubsection \<open>Proof structure\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>{\<close> "begin explicit proof block"
     (Scan.succeed (Toplevel.proof Proof.begin_block));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>}\<close> "end explicit proof block"
     (Scan.succeed (Toplevel.proof Proof.end_block));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>next\<close> "enter next proof block"
     (Scan.succeed (Toplevel.proof Proof.next_block));
 
 in end\<close>
 
 
 subsubsection \<open>End proof\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>qed\<close> "conclude proof"
     (Scan.option Method.parse >> (fn m =>
      (Option.map Method.report m;
       Isar_Cmd.qed m)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>by\<close> "terminal backward proof"
     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
      (Method.report m1;
       Option.map Method.report m2;
       Isar_Cmd.terminal_proof (m1, m2))));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>..\<close> "default proof"
     (Scan.succeed Isar_Cmd.default_proof);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>.\<close> "immediate proof"
     (Scan.succeed Isar_Cmd.immediate_proof);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>done\<close> "done proof"
     (Scan.succeed Isar_Cmd.done_proof);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>sorry\<close> "skip proof (quick-and-dirty mode only!)"
     (Scan.succeed Isar_Cmd.skip_proof);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>\<proof>\<close> "dummy proof (quick-and-dirty mode only!)"
     (Scan.succeed Isar_Cmd.skip_proof);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
     (Scan.succeed Toplevel.forget_proof);
 
 in end\<close>
 
 
 subsubsection \<open>Proof steps\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>defer\<close> "shuffle internal proof state"
     (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>prefer\<close> "shuffle internal proof state"
     (Parse.nat >> (Toplevel.proof o Proof.prefer));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>apply\<close> "initial goal refinement step (unstructured)"
     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>apply_end\<close> "terminal goal refinement step (unstructured)"
     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>proof\<close> "backward proof step"
     (Scan.option Method.parse >> (fn m =>
       (Option.map Method.report m;
        Toplevel.proof (fn state =>
          let
           val state' = state |> Proof.proof m |> Seq.the_result "";
           val _ =
             Output.information
               (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state'));
         in state' end))))
 
 in end\<close>
 
 
 subsubsection \<open>Subgoal focus\<close>
 
 ML \<open>
 local
 
 val opt_fact_binding =
   Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
     Binding.empty_atts;
 
 val for_params =
   Scan.optional
     (\<^keyword>\<open>for\<close> |--
       Parse.!!! ((Scan.option Parse.dots >> is_some) --
         (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
     (false, []);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>subgoal\<close>
     "focus on first subgoal within backward refinement"
     (opt_fact_binding -- (Scan.option (\<^keyword>\<open>premises\<close> |-- Parse.!!! opt_fact_binding)) --
       for_params >> (fn ((a, b), c) =>
         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
 
 in end\<close>
 
 
 subsubsection \<open>Calculation\<close>
 
 ML \<open>
 local
 
 val calculation_args =
   Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\<open>)\<close>)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>also\<close> "combine calculation and current facts"
     (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>finally\<close>
     "combine calculation and current facts, exhibit result"
     (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>moreover\<close> "augment calculation by current facts"
     (Scan.succeed (Toplevel.proof' Calculation.moreover));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ultimately\<close>
     "augment calculation by current facts, exhibit result"
     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_trans_rules\<close> "print transitivity rules"
     (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
 
 in end\<close>
 
 
 subsubsection \<open>Proof navigation\<close>
 
 ML \<open>
 local
 
 fun report_back () =
   Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>back\<close> "explicit backtracking of proof command"
     (Scan.succeed
      (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
       Toplevel.skip_proof report_back));
 
 in end\<close>
 
 
 subsection \<open>Diagnostic commands (for interactive mode only)\<close>
 
 ML \<open>
 local
 
 val opt_modes =
   Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>help\<close>
     "retrieve outer syntax commands according to name patterns"
     (Scan.repeat Parse.name >>
       (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_commands\<close> "print outer syntax commands"
     (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_options\<close> "print configuration options"
     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
     "print context of local theory target"
     (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
     "print logical theory contents"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_definitions\<close>
     "print dependencies of definitional theory content"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_syntax\<close>
     "print inner syntax of context"
     (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_defn_rules\<close>
     "print definitional rewrite rules of context"
     (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_abbrevs\<close>
     "print constant abbreviations of context"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_theorems\<close>
     "print theorems of local theory or proof context"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_locales\<close>
     "print locales of this theory"
     (Parse.opt_bang >> (fn verbose =>
       Toplevel.keep (fn state =>
         let val thy = Toplevel.theory_of state
         in Pretty.writeln (Locale.pretty_locales thy verbose) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_classes\<close>
     "print classes of this theory"
     (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_locale\<close>
     "print locale of this theory"
     (Parse.opt_bang -- Parse.name_position >> (fn (show_facts, raw_name) =>
       Toplevel.keep (fn state =>
         let
           val thy = Toplevel.theory_of state;
           val name = Locale.check thy raw_name;
         in Pretty.writeln (Locale.pretty_locale thy show_facts name) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
     "print interpretations of locale for this theory or proof context"
     (Parse.name_position >> (fn raw_name =>
       Toplevel.keep (fn state =>
         let
           val ctxt = Toplevel.context_of state;
           val thy = Toplevel.theory_of state;
           val name = Locale.check thy raw_name;
         in Pretty.writeln (Locale.pretty_registrations ctxt name) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_attributes\<close>
     "print attributes of this theory"
     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_simpset\<close>
     "print context of Simplifier"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_rules\<close> "print intro/elim rules"
     (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_methods\<close> "print methods of this theory"
     (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_antiquotations\<close>
     "print document antiquotations"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_ML_antiquotations\<close>
     "print ML antiquotations"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>locale_deps\<close> "visualize locale dependencies"
     (Scan.succeed
       (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
         Locale.pretty_locale_deps thy
         |> map (fn {name, parents, body} =>
           ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
         |> Graph_Display.display_graph_old))));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_term_bindings\<close>
     "print term bindings of proof context"
     (Scan.succeed
       (Toplevel.keep
         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
     (Scan.succeed
       (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
     "print theorems as long statements"
     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thm\<close> "print theorems"
     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>prf\<close> "print proof terms of theorems"
     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>full_prf\<close> "print full proof terms of theorems"
     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>prop\<close> "read and print proposition"
     (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>term\<close> "read and print term"
     (opt_modes -- Parse.term >> Isar_Cmd.print_term);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>typ\<close> "read and print type"
     (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.sort))
       >> Isar_Cmd.print_type);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_codesetup\<close> "print code generator setup"
     (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
     "print current proof state (if present)"
     (opt_modes >> (fn modes =>
       Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
     (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
 
 in end\<close>
 
 
 subsection \<open>Dependencies\<close>
 
 ML \<open>
 local
 
 val theory_bounds =
   Parse.theory_name >> single ||
   (\<^keyword>\<open>(\<close> |-- Parse.enum "|" Parse.theory_name --| \<^keyword>\<open>)\<close>);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thy_deps\<close> "visualize theory dependencies"
     (Scan.option theory_bounds -- Scan.option theory_bounds >>
       (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
 
 
 val class_bounds =
   Parse.sort >> single ||
   (\<^keyword>\<open>(\<close> |-- Parse.enum "|" Parse.sort --| \<^keyword>\<open>)\<close>);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>class_deps\<close> "visualize class dependencies"
     (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
       Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
 
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close>
     "print theorem dependencies (immediate non-transitive)"
     (Parse.thms1 >> (fn args =>
       Toplevel.keep (fn st =>
         let
           val thy = Toplevel.theory_of st;
           val ctxt = Toplevel.context_of st;
         in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thm_oracles\<close>
     "print all oracles used in theorems (full graph of transitive dependencies)"
     (Parse.thms1 >> (fn args =>
       Toplevel.keep (fn st =>
         let
           val ctxt = Toplevel.context_of st;
           val thms = Attrib.eval_thms ctxt args;
         in Pretty.writeln (Thm_Deps.pretty_thm_oracles ctxt thms) end)));
 
 val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>unused_thms\<close> "find unused theorems"
     (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
         Toplevel.keep (fn st =>
           let
             val thy = Toplevel.theory_of st;
             val ctxt = Toplevel.context_of st;
             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
             val check = Theory.check {long = false} ctxt;
           in
             Thm_Deps.unused_thms_cmd
               (case opt_range of
                 NONE => (Theory.parents_of thy, [thy])
               | SOME (xs, NONE) => (map check xs, [thy])
               | SOME (xs, SOME ys) => (map check xs, map check ys))
             |> map pretty_thm |> Pretty.writeln_chunks
           end)));
 
 in end\<close>
 
 
 subsubsection \<open>Find consts and theorems\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>find_consts\<close>
     "find constants by name / type patterns"
     (Find_Consts.query_parser >> (fn spec =>
       Toplevel.keep (fn st =>
         Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
 
 val options =
   Scan.optional
     (Parse.$$$ "(" |--
       Parse.!!! (Scan.option Parse.nat --
         Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
     (NONE, true);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>find_theorems\<close>
     "find theorems meeting specified criteria"
     (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
       Toplevel.keep (fn st =>
         Pretty.writeln
           (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
 
 in end\<close>
 
 
 subsection \<open>Code generation\<close>
 
 ML \<open>
 local
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_datatype\<close>
     "define set of code datatype constructors"
     (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
 
 in end\<close>
 
 
 subsection \<open>Extraction of programs from proofs\<close>
 
 ML \<open>
 local
 
 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>realizers\<close>
     "specify realizers for primitive axioms / theorems, together with correctness proof"
     (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
      (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>realizability\<close>
     "add equations characterizing realizability"
     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>extract_type\<close>
     "add equations characterizing type of extracted program"
     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>extract\<close> "extract terms from proofs"
     (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
 
 in end\<close>
 
 
 section \<open>Auxiliary lemmas\<close>
 
 subsection \<open>Meta-level connectives in assumptions\<close>
 
 lemma meta_mp:
   assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
   shows "PROP Q"
     by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
 
 lemmas meta_impE = meta_mp [elim_format]
 
 lemma meta_spec:
   assumes "\<And>x. PROP P x"
   shows "PROP P x"
     by (rule \<open>\<And>x. PROP P x\<close>)
 
 lemmas meta_allE = meta_spec [elim_format]
 
 lemma swap_params:
   "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
 
 lemma equal_allI:
   \<open>(\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)\<close> if \<open>\<And>x. PROP P x \<equiv> PROP Q x\<close>
   by (simp only: that)
 
 
 subsection \<open>Meta-level conjunction\<close>
 
 lemma all_conjunction:
   "(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))"
 proof
   assume conj: "\<And>x. PROP A x &&& PROP B x"
   show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
   proof -
     fix x
     from conj show "PROP A x" by (rule conjunctionD1)
     from conj show "PROP B x" by (rule conjunctionD2)
   qed
 next
   assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
   fix x
   show "PROP A x &&& PROP B x"
   proof -
     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
   qed
 qed
 
 lemma imp_conjunction:
   "(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))"
 proof
   assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C"
   show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
   proof -
     assume "PROP A"
     from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1)
     from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2)
   qed
 next
   assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
   assume "PROP A"
   show "PROP B &&& PROP C"
   proof -
     from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1])
     from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2])
   qed
 qed
 
 lemma conjunction_imp:
   "(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)"
 proof
   assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C"
   assume ab: "PROP A" "PROP B"
   show "PROP C"
   proof (rule r)
     from ab show "PROP A &&& PROP B" .
   qed
 next
   assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C"
   assume conj: "PROP A &&& PROP B"
   show "PROP C"
   proof (rule r)
     from conj show "PROP A" by (rule conjunctionD1)
     from conj show "PROP B" by (rule conjunctionD2)
   qed
 qed
 
 declare [[ML_write_global = false]]
 
 end