diff --git a/src/Pure/Concurrent/synchronized.ML b/src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML
+++ b/src/Pure/Concurrent/synchronized.ML
@@ -1,122 +1,144 @@
 (*  Title:      Pure/Concurrent/synchronized.ML
     Author:     Fabian Immler and Makarius
 
 Synchronized variables.
 *)
 
 signature SYNCHRONIZED =
 sig
   type 'a var
   val var: string -> 'a -> 'a var
   val value: 'a var -> 'a
   val assign: 'a var -> 'a -> unit
   val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
   val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
   type 'a cache
   val cache: (unit -> 'a) -> 'a cache
   val cache_peek: 'a cache -> 'a option
-  val cache_eval: 'a cache -> 'a
+  val cache_eval: {persistent: bool} -> 'a cache -> 'a
 end;
 
 structure Synchronized: SYNCHRONIZED =
 struct
 
 (* state variable *)
 
 datatype 'a state =
     Immutable of 'a
   | Mutable of {lock: Thread.Mutex.mutex, cond: Thread.ConditionVar.conditionVar, content: 'a};
 
 fun init_state x =
   Mutable {lock = Thread.Mutex.mutex (), cond = Thread.ConditionVar.conditionVar (), content = x};
 
 fun immutable_fail name = raise Fail ("Illegal access to immutable value " ^ name);
 
 abstype 'a var = Var of {name: string, state: 'a state Unsynchronized.ref}
 with
 
 fun var name x =
   Var {name = name, state = Unsynchronized.ref (init_state x)};
 
 fun value (Var {name, state}) =
   (case ! state of
     Immutable x => x
   | Mutable {lock, ...} =>
       Multithreading.synchronized name lock (fn () =>
         (case ! state of
           Immutable x => x
         | Mutable {content, ...} => content)));
 
 fun assign (Var {name, state}) x =
   (case ! state of
     Immutable _ => immutable_fail name
   | Mutable {lock, cond, ...} =>
       Multithreading.synchronized name lock (fn () =>
         (case ! state of
           Immutable _ => immutable_fail name
         | Mutable _ =>
             Thread_Attributes.uninterruptible_body (fn _ =>
              (state := Immutable x; RunCall.clearMutableBit state;
                Thread.ConditionVar.broadcast cond)))));
 
 
 (* synchronized access *)
 
 fun timed_access (Var {name, state}) time_limit f =
   (case ! state of
     Immutable _ => immutable_fail name
   | Mutable {lock, cond, ...} =>
       Multithreading.synchronized name lock (fn () =>
         let
           fun try_change () =
             (case ! state of
               Immutable _ => immutable_fail name
             | Mutable {content = x, ...} =>
                 (case f x of
                   NONE =>
                     (case Multithreading.sync_wait (time_limit x) cond lock of
                       Exn.Res true => try_change ()
                     | Exn.Res false => NONE
                     | Exn.Exn exn => Exn.reraise exn)
                 | SOME (y, x') =>
                     Thread_Attributes.uninterruptible_body (fn _ =>
                       (state := Mutable {lock = lock, cond = cond, content = x'};
                         Thread.ConditionVar.broadcast cond; SOME y))));
         in try_change () end));
 
 fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
 
 
 (* unconditional change *)
 
 fun change_result var f = guarded_access var (SOME o f);
 fun change var f = change_result var (fn x => ((), f x));
 
 end;
 
 
 (* cached evaluation via weak_ref *)
 
+local
+
+datatype 'a cache_state =
+    Undef
+  | Value of 'a
+  | Weak_Ref of 'a Unsynchronized.weak_ref;
+
+fun peek Undef = NONE
+  | peek (Value x) = SOME x
+  | peek (Weak_Ref r) = Unsynchronized.weak_peek r;
+
+fun weak_active (Weak_Ref r) = Unsynchronized.weak_active r
+  | weak_active _ = false;
+
+in
+
 abstype 'a cache =
-  Cache of {expr: unit -> 'a, var: 'a Unsynchronized.weak_ref option var}
+  Cache of {expr: unit -> 'a, var: 'a cache_state var}
 with
 
 fun cache expr =
-  Cache {expr = expr, var = var "Synchronized.cache" NONE};
-
-fun cache_peek (Cache {var, ...}) =
-  Option.mapPartial Unsynchronized.weak_peek (value var);
+  Cache {expr = expr, var = var "Synchronized.cache" Undef};
 
-fun cache_eval (Cache {expr, var}) =
+fun cache_peek (Cache {var, ...}) = peek (value var);
+
+fun cache_eval {persistent} (Cache {expr, var}) =
   change_result var (fn state =>
-    (case Option.mapPartial Unsynchronized.weak_peek state of
-      SOME result => (result, state)
-    | NONE =>
-        let val result = expr ()
-        in (result, SOME (Unsynchronized.weak_ref result)) end));
+    let
+      val result =
+        (case peek state of
+          SOME result => result
+        | NONE => expr ());
+      val state' =
+        if persistent then Value result
+        else if weak_active state then state
+        else Weak_Ref (Unsynchronized.weak_ref result);
+    in (result, state') end);
 
 end;
 
 end;
+
+end;
diff --git a/src/Pure/Syntax/syntax.ML b/src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML
+++ b/src/Pure/Syntax/syntax.ML
@@ -1,692 +1,701 @@
 (*  Title:      Pure/Syntax/syntax.ML
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Standard Isabelle syntax, based on arbitrary context-free grammars
 (specified by mixfix declarations).
 *)
 
 signature SYNTAX =
 sig
   type operations
   val install_operations: operations -> theory -> theory
   val root: string Config.T
   val ambiguity_warning: bool Config.T
   val ambiguity_limit: int Config.T
   val encode_input: Input.source -> XML.tree
   val implode_input: Input.source -> string
   val read_input_pos: string -> Position.T
   val read_input: string -> Input.source
   val parse_input: Proof.context -> (XML.tree list -> 'a) ->
     (bool -> Markup.T) -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   val parse_sort: Proof.context -> string -> sort
   val parse_typ: Proof.context -> string -> typ
   val parse_term: Proof.context -> string -> term
   val parse_prop: Proof.context -> string -> term
   val unparse_sort: Proof.context -> sort -> Pretty.T
   val unparse_classrel: Proof.context -> class list -> Pretty.T
   val unparse_arity: Proof.context -> arity -> Pretty.T
   val unparse_typ: Proof.context -> typ -> Pretty.T
   val unparse_term: Proof.context -> term -> Pretty.T
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
   val check_term: Proof.context -> term -> term
   val check_prop: Proof.context -> term -> term
   val check_typs: Proof.context -> typ list -> typ list
   val check_terms: Proof.context -> term list -> term list
   val check_props: Proof.context -> term list -> term list
   val uncheck_sort: Proof.context -> sort -> sort
   val uncheck_arity: Proof.context -> arity -> arity
   val uncheck_classrel: Proof.context -> class list -> class list
   val uncheck_typs: Proof.context -> typ list -> typ list
   val uncheck_terms: Proof.context -> term list -> term list
   val read_sort: Proof.context -> string -> sort
   val read_typ: Proof.context -> string -> typ
   val read_term: Proof.context -> string -> term
   val read_prop: Proof.context -> string -> term
   val read_typs: Proof.context -> string list -> typ list
   val read_terms: Proof.context -> string list -> term list
   val read_props: Proof.context -> string list -> term list
   val read_sort_global: theory -> string -> sort
   val read_typ_global: theory -> string -> typ
   val read_term_global: theory -> string -> term
   val read_prop_global: theory -> string -> term
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_typ: Proof.context -> typ -> Pretty.T
   val pretty_sort: Proof.context -> sort -> Pretty.T
   val pretty_classrel: Proof.context -> class list -> Pretty.T
   val pretty_arity: Proof.context -> arity -> Pretty.T
   val string_of_term: Proof.context -> term -> string
   val string_of_typ: Proof.context -> typ -> string
   val string_of_sort: Proof.context -> sort -> string
   val string_of_classrel: Proof.context -> class list -> string
   val string_of_arity: Proof.context -> arity -> string
   val is_pretty_global: Proof.context -> bool
   val set_pretty_global: bool -> Proof.context -> Proof.context
   val init_pretty_global: theory -> Proof.context
   val init_pretty: Context.generic -> Proof.context
   val pretty_term_global: theory -> term -> Pretty.T
   val pretty_typ_global: theory -> typ -> Pretty.T
   val pretty_sort_global: theory -> sort -> Pretty.T
   val string_of_term_global: theory -> term -> string
   val string_of_typ_global: theory -> typ -> string
   val string_of_sort_global: theory -> sort -> string
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T list
   type syntax
+  val cache_persistent: bool Unsynchronized.ref
+  val cache_syntax: syntax -> unit
   val eq_syntax: syntax * syntax -> bool
   datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
   val get_approx: syntax -> string -> approx option
   val lookup_const: syntax -> string -> string option
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
   val parse: syntax -> string -> Lexicon.token list -> Parser.parsetree list
   val parse_ast_translation: syntax -> string -> (Proof.context -> Ast.ast list -> Ast.ast) option
   val parse_rules: syntax -> string -> (Ast.ast * Ast.ast) list
   val parse_translation: syntax -> string -> (Proof.context -> term list -> term) option
   val print_translation: syntax -> string ->
     Proof.context -> typ -> term list -> term  (*exception Match*)
   val print_rules: syntax -> string -> (Ast.ast * Ast.ast) list
   val print_ast_translation: syntax -> string ->
     Proof.context -> Ast.ast list -> Ast.ast  (*exception Match*)
   val prtabs: syntax -> Printer.prtabs
   type mode
   val mode_default: mode
   val mode_input: mode
   val empty_syntax: syntax
   val merge_syntax: syntax * syntax -> syntax
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
   datatype 'a trrule =
     Parse_Rule of 'a * 'a |
     Print_Rule of 'a * 'a |
     Parse_Print_Rule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val update_trfuns:
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_const_gram: bool -> string list ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_trrules: Ast.ast trrule list -> syntax -> syntax
   val remove_trrules: Ast.ast trrule list -> syntax -> syntax
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
 end;
 
 structure Syntax: SYNTAX =
 struct
 
 
 (** inner syntax operations **)
 
 (* operations *)
 
 type operations =
  {parse_sort: Proof.context -> string -> sort,
   parse_typ: Proof.context -> string -> typ,
   parse_term: Proof.context -> string -> term,
   parse_prop: Proof.context -> string -> term,
   unparse_sort: Proof.context -> sort -> Pretty.T,
   unparse_typ: Proof.context -> typ -> Pretty.T,
   unparse_term: Proof.context -> term -> Pretty.T,
   check_typs: Proof.context -> typ list -> typ list,
   check_terms: Proof.context -> term list -> term list,
   check_props: Proof.context -> term list -> term list,
   uncheck_typs: Proof.context -> typ list -> typ list,
   uncheck_terms: Proof.context -> term list -> term list};
 
 structure Operations = Theory_Data
 (
   type T = operations option;
   val empty = NONE;
   val merge = merge_options;
 );
 
 fun install_operations ops =
   Operations.map
     (fn NONE => SOME ops
       | SOME _ => raise Fail "Inner syntax operations already installed");
 
 fun operation which ctxt x =
   (case Operations.get (Proof_Context.theory_of ctxt) of
     NONE => raise Fail "Inner syntax operations not installed"
   | SOME ops => which ops ctxt x);
 
 
 (* configuration options *)
 
 val root = Config.declare_string ("syntax_root", \<^here>) (K "any");
 val ambiguity_warning = Config.declare_bool ("syntax_ambiguity_warning", \<^here>) (K true);
 val ambiguity_limit = Config.declare_int ("syntax_ambiguity_limit", \<^here>) (K 10);
 
 
 (* formal input *)
 
 fun encode_input source =
   let
     val delimited = Input.is_delimited source;
     val pos = Input.pos_of source;
     val text = Input.text_of source;
   in XML.Elem (Markup.input delimited (Position.properties_of pos), [XML.Text text]) end;
 
 val implode_input = encode_input #> YXML.string_of;
 
 local
 
 fun input_range (XML.Elem ((name, props), _)) =
       if name = Markup.inputN
       then (Markup.is_delimited props, Position.range_of_properties props)
       else (false, Position.no_range)
   | input_range (XML.Text _) = (false, Position.no_range);
 
 fun input_source tree =
   let
     val text = XML.content_of [tree];
     val (delimited, range) = input_range tree;
   in Input.source delimited text range end;
 
 in
 
 fun read_input_pos str = #1 (#2 (input_range (YXML.parse str handle Fail msg => error msg)));
 
 fun read_input str = input_source (YXML.parse str handle Fail msg => error msg);
 
 fun parse_input ctxt decode markup parse str =
   let
     fun parse_tree tree =
       let
         val source = input_source tree;
         val syms = Input.source_explode source;
         val pos = Input.pos_of source;
         val _ =
           Context_Position.reports ctxt
             [(pos, Markup.cartouche), (pos, markup (Input.is_delimited source))];
         val _ =
           if Options.default_bool "update_inner_syntax_cartouches" then
             Context_Position.report_text ctxt
               pos Markup.update (cartouche (Symbol_Pos.content syms))
           else ();
       in parse (syms, pos) end;
   in
     (case YXML.parse_body str handle Fail msg => error msg of
       body as [tree as XML.Elem ((name, _), _)] =>
         if name = Markup.inputN then parse_tree tree else decode body
     | [tree as XML.Text _] => parse_tree tree
     | body => decode body)
   end;
 
 end;
 
 
 (* (un)parsing *)
 
 val parse_sort = operation #parse_sort;
 val parse_typ = operation #parse_typ;
 val parse_term = operation #parse_term;
 val parse_prop = operation #parse_prop;
 val unparse_sort = operation #unparse_sort;
 val unparse_typ = operation #unparse_typ;
 val unparse_term = operation #unparse_term;
 
 
 (* (un)checking *)
 
 val check_typs = operation #check_typs;
 val check_terms = operation #check_terms;
 val check_props = operation #check_props;
 
 val check_typ = singleton o check_typs;
 val check_term = singleton o check_terms;
 val check_prop = singleton o check_props;
 
 val uncheck_typs = operation #uncheck_typs;
 val uncheck_terms = operation #uncheck_terms;
 
 
 (* derived operations for algebra of sorts *)
 
 local
 
 fun map_sort f S =
   (case f (TFree ("", S)) of
     TFree ("", S') => S'
   | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
 
 in
 
 val check_sort = map_sort o check_typ;
 val uncheck_sort = map_sort o singleton o uncheck_typs;
 
 end;
 
 
 val uncheck_classrel = map o singleton o uncheck_sort;
 
 fun unparse_classrel ctxt cs = Pretty.block (flat
   (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs)));
 
 fun uncheck_arity ctxt (a, Ss, S) =
   let
     val T = Type (a, replicate (length Ss) dummyT);
     val a' =
       (case singleton (uncheck_typs ctxt) T of
         Type (a', _) => a'
       | T => raise TYPE ("uncheck_arity", [T], []));
     val Ss' = map (uncheck_sort ctxt) Ss;
     val S' = uncheck_sort ctxt S;
   in (a', Ss', S') end;
 
 fun unparse_arity ctxt (a, Ss, S) =
   let
     val prtT = unparse_typ ctxt (Type (a, []));
     val dom =
       if null Ss then []
       else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1];
   in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end;
 
 
 (* read = parse + check *)
 
 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
 
 fun read_typs ctxt =
   grouped 10 Par_List.map_independent (parse_typ ctxt) #> check_typs ctxt;
 
 fun read_terms ctxt =
   grouped 10 Par_List.map_independent (parse_term ctxt) #> check_terms ctxt;
 
 fun read_props ctxt =
   grouped 10 Par_List.map_independent (parse_prop ctxt) #> check_props ctxt;
 
 val read_typ = singleton o read_typs;
 val read_term = singleton o read_terms;
 val read_prop = singleton o read_props;
 
 val read_sort_global = read_sort o Proof_Context.init_global;
 val read_typ_global = read_typ o Proof_Context.init_global;
 val read_term_global = read_term o Proof_Context.init_global;
 val read_prop_global = read_prop o Proof_Context.init_global;
 
 
 (* pretty = uncheck + unparse *)
 
 fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt;
 fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt;
 fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt;
 fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt;
 fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt;
 
 val string_of_term = Pretty.string_of oo pretty_term;
 val string_of_typ = Pretty.string_of oo pretty_typ;
 val string_of_sort = Pretty.string_of oo pretty_sort;
 val string_of_classrel = Pretty.string_of oo pretty_classrel;
 val string_of_arity = Pretty.string_of oo pretty_arity;
 
 
 (* global pretty printing *)
 
 val pretty_global = Config.declare_bool ("Syntax.pretty_global", \<^here>) (K false);
 val is_pretty_global = Config.apply pretty_global;
 val set_pretty_global = Config.put pretty_global;
 val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
 val init_pretty = Context.cases init_pretty_global I;
 
 val pretty_term_global = pretty_term o init_pretty_global;
 val pretty_typ_global = pretty_typ o init_pretty_global;
 val pretty_sort_global = pretty_sort o init_pretty_global;
 
 val string_of_term_global = string_of_term o init_pretty_global;
 val string_of_typ_global = string_of_typ o init_pretty_global;
 val string_of_sort_global = string_of_sort o init_pretty_global;
 
 
 (* derived operations *)
 
 fun pretty_flexpair ctxt (t, u) =
   [pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, pretty_term ctxt u];
 
 
 
 (** tables of translation functions **)
 
 (* parse (ast) translations *)
 
 fun err_dup_trfun name c =
   error ("More than one " ^ name ^ " for " ^ quote c);
 
 fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
 
 fun remove_trtab trfuns = fold (Symtab.remove Syntax_Ext.eq_trfun) trfuns;
 
 fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
   handle Symtab.DUP c => err_dup_trfun name c;
 
 fun merge_trtabs name tab1 tab2 = Symtab.merge Syntax_Ext.eq_trfun (tab1, tab2)
   handle Symtab.DUP c => err_dup_trfun name c;
 
 
 (* print (ast) translations *)
 
 fun apply_tr' tab c ctxt T args =
   let
     val fns = map fst (Symtab.lookup_list tab c);
     fun app_first [] = raise Match
       | app_first (f :: fs) = f ctxt T args handle Match => app_first fs;
   in app_first fns end;
 
 fun apply_ast_tr' tab c ctxt args =
   let
     val fns = map fst (Symtab.lookup_list tab c);
     fun app_first [] = raise Match
       | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
   in app_first fns end;
 
 fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syntax_Ext.eq_trfun) trfuns;
 fun remove_tr'tab trfuns = fold (Symtab.remove_list Syntax_Ext.eq_trfun) trfuns;
 fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syntax_Ext.eq_trfun (tab1, tab2);
 
 
 
 (** tables of translation rules **)
 
 type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
 
 fun dest_ruletab tab = maps snd (Symtab.dest tab);
 
 val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r));
 val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
 fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
 
 
 
 (** datatype syntax **)
 
 datatype syntax =
   Syntax of {
     input: Syntax_Ext.xprod list,
     lexicon: Scan.lexicon,
     gram: Parser.gram Synchronized.cache,
     consts: string Symtab.table,
     prmodes: string list,
     parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
     parse_ruletab: ruletab,
     parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
     print_trtab: ((Proof.context -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     prtabs: Printer.prtabs} * stamp;
 
+val cache_persistent = Unsynchronized.ref false;
+
+fun cache_eval (gram: Parser.gram Synchronized.cache) =
+  Synchronized.cache_eval {persistent = ! cache_persistent} gram;
+
+fun cache_syntax (Syntax ({gram, ...}, _)) = ignore (cache_eval gram);
+
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
 
 datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int};
 fun get_approx (Syntax ({prtabs, ...}, _)) c =
   (case Printer.get_infix prtabs c of
     SOME infx => SOME (Infix infx)
   | NONE =>
       (case Printer.get_prefix prtabs c of
         SOME prfx => SOME prfx
       | NONE => Printer.get_binder prtabs c)
       |> Option.map Prefix);
 
 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
-fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Synchronized.cache_eval gram);
+fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram);
 
 fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
 fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
 fun parse_rules (Syntax ({parse_ruletab, ...}, _)) = Symtab.lookup_list parse_ruletab;
 fun print_translation (Syntax ({print_trtab, ...}, _)) = apply_tr' print_trtab;
 fun print_rules (Syntax ({print_ruletab, ...}, _)) = Symtab.lookup_list print_ruletab;
 fun print_ast_translation (Syntax ({print_ast_trtab, ...}, _)) = apply_ast_tr' print_ast_trtab;
 
 fun prtabs (Syntax ({prtabs, ...}, _)) = prtabs;
 
 type mode = string * bool;
 val mode_default = ("", true);
 val mode_input = (Print_Mode.input, true);
 
 fun extend_gram new_xprods old_xprods gram =
   Synchronized.cache (fn () =>
     Parser.make_gram new_xprods old_xprods (Synchronized.cache_peek gram));
 
 fun new_gram new_xprods =
   Synchronized.cache (fn () => Parser.make_gram new_xprods [] NONE);
 
 
 (* empty_syntax *)
 
 val empty_syntax = Syntax
   ({input = [],
     lexicon = Scan.empty_lexicon,
     gram = Synchronized.cache (fn () => Parser.empty_gram),
     consts = Symtab.empty,
     prmodes = [],
     parse_ast_trtab = Symtab.empty,
     parse_ruletab = Symtab.empty,
     parse_trtab = Symtab.empty,
     print_trtab = Symtab.empty,
     print_ruletab = Symtab.empty,
     print_ast_trtab = Symtab.empty,
     prtabs = Printer.empty_prtabs}, stamp ());
 
 
 (* update_syntax *)
 
 fun update_const (c, b) tab =
   if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
   then tab
   else Symtab.update (c, b) tab;
 
 fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   let
     val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab,
       parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs;
     val Syntax_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation,
       parse_rules, parse_translation, print_translation, print_rules,
       print_ast_translation} = syn_ext;
     val new_xprods =
       if inout then distinct (op =) (filter_out (member (op =) input) xprods) else [];
     fun if_inout xs = if inout then xs else [];
   in
     Syntax
     ({input = new_xprods @ input,
       lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
       gram = if null new_xprods then gram else extend_gram new_xprods input gram,
       consts = fold update_const consts2 consts1,
       prmodes = insert (op =) mode prmodes,
       parse_ast_trtab =
         update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
       parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab,
       parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab,
       print_trtab = update_tr'tab print_translation print_trtab,
       print_ruletab = update_ruletab print_rules print_ruletab,
       print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab,
       prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ())
   end;
 
 
 (* remove_syntax *)
 
 fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   let
     val Syntax_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules,
       parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext;
     val {input, lexicon, gram, consts, prmodes, parse_ast_trtab, parse_ruletab,
       parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs;
     val input' = if inout then subtract (op =) xprods input else input;
     val changed = length input <> length input';
     fun if_inout xs = if inout then xs else [];
   in
     Syntax
     ({input = input',
       lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon,
       gram = if changed then new_gram input' else gram,
       consts = consts,
       prmodes = prmodes,
       parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
       parse_ruletab = remove_ruletab (if_inout parse_rules) parse_ruletab,
       parse_trtab = remove_trtab (if_inout parse_translation) parse_trtab,
       print_trtab = remove_tr'tab print_translation print_trtab,
       print_ruletab = remove_ruletab print_rules print_ruletab,
       print_ast_trtab = remove_tr'tab print_ast_translation print_ast_trtab,
       prtabs = Printer.remove_prtabs mode xprods prtabs}, stamp ())
   end;
 
 
 (* merge_syntax *)
 
 fun merge_syntax (Syntax (tabs1, _), Syntax (tabs2, _)) =
   let
     val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1,
       prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
       parse_trtab = parse_trtab1, print_trtab = print_trtab1, print_ruletab = print_ruletab1,
       print_ast_trtab = print_ast_trtab1, prtabs = prtabs1} = tabs1;
 
     val {input = input2, lexicon = lexicon2, gram = gram2, consts = consts2,
       prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
       parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2,
       print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2;
 
     val (input', gram') =
       if pointer_eq (input1, input2) then (input1, gram1)
       else
         (case subtract (op =) input1 input2 of
           [] => (input1, gram1)
         | new_xprods2 =>
             if subset (op =) (input1, input2) then (input2, gram2)
             else
               let
                 val input' = new_xprods2 @ input1;
                 val gram' = new_gram input';
               in (input', gram') end);
   in
     Syntax
     ({input = input',
       lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
       gram = gram',
       consts = Symtab.merge (K true) (consts1, consts2),
       prmodes = Library.merge (op =) (prmodes1, prmodes2),
       parse_ast_trtab =
         merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
       parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
       parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
       print_trtab = merge_tr'tabs print_trtab1 print_trtab2,
       print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
       print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2,
       prtabs = Printer.merge_prtabs prtabs1 prtabs2}, stamp ())
   end;
 
 
 
 (** print syntax **)
 
 local
 
 fun pretty_strs_qs name strs =
   Pretty.strs (name :: map quote (sort_strings strs));
 
 fun pretty_gram (Syntax (tabs, _)) =
   let
     val {lexicon, prmodes, gram, ...} = tabs;
     val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
   in
     [Pretty.block (Pretty.breaks
       (Pretty.str "lexicon:" :: map (Pretty.quote o Pretty.keyword1) (Scan.dest_lexicon lexicon))),
-      Pretty.big_list "productions:" (Parser.pretty_gram (Synchronized.cache_eval gram)),
+      Pretty.big_list "productions:" (Parser.pretty_gram (cache_eval gram)),
       pretty_strs_qs "print modes:" prmodes']
   end;
 
 fun pretty_trans (Syntax (tabs, _)) =
   let
     fun pretty_tab name tab =
       pretty_strs_qs name (sort_strings (Symtab.keys tab));
 
     fun pretty_ruletab name tab =
       Pretty.big_list name (map (Pretty.item o single o Ast.pretty_rule) (dest_ruletab tab));
 
     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
       print_ruletab, print_ast_trtab, ...} = tabs;
   in
    [pretty_tab "consts:" consts,
     pretty_tab "parse_ast_translation:" parse_ast_trtab,
     pretty_ruletab "parse_rules:" parse_ruletab,
     pretty_tab "parse_translation:" parse_trtab,
     pretty_tab "print_translation:" print_trtab,
     pretty_ruletab "print_rules:" print_ruletab,
     pretty_tab "print_ast_translation:" print_ast_trtab]
   end;
 
 in
 
 fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn);
 fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn);
 fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
 
 end;
 
 
 
 (** prepare translation rules **)
 
 (* rules *)
 
 datatype 'a trrule =
   Parse_Rule of 'a * 'a |
   Print_Rule of 'a * 'a |
   Parse_Print_Rule of 'a * 'a;
 
 fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y)
   | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y)
   | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y);
 
 fun parse_rule (Parse_Rule pats) = SOME pats
   | parse_rule (Print_Rule _) = NONE
   | parse_rule (Parse_Print_Rule pats) = SOME pats;
 
 fun print_rule (Parse_Rule _) = NONE
   | print_rule (Print_Rule pats) = SOME (swap pats)
   | print_rule (Parse_Print_Rule pats) = SOME (swap pats);
 
 
 (* check_rules *)
 
 local
 
 fun check_rule rule =
   (case Ast.rule_error rule of
     SOME msg =>
       error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
         Pretty.string_of (Ast.pretty_rule rule))
   | NONE => rule);
 
 in
 
 fun check_rules rules =
  (map check_rule (map_filter parse_rule rules),
   map check_rule (map_filter print_rule rules));
 
 end;
 
 
 
 (** modify syntax **)
 
 val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns;
 
 fun update_type_gram add prmode decls =
   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
 
 fun update_const_gram add logical_types prmode decls =
   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls);
 
 val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 
 
 open Lexicon.Syntax;
 
 end;
diff --git a/src/Pure/System/isabelle_process.ML b/src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML
+++ b/src/Pure/System/isabelle_process.ML
@@ -1,236 +1,238 @@
 (*  Title:      Pure/System/isabelle_process.ML
     Author:     Makarius
 
 Isabelle process wrapper.
 *)
 
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
   val init_options: unit -> unit
   val init_options_interactive: unit -> unit
   val init: unit -> unit
   val init_build: unit -> unit
 end;
 
 structure Isabelle_Process: ISABELLE_PROCESS =
 struct
 
 (* print mode *)
 
 val isabelle_processN = "isabelle_process";
 
 fun is_active () = Print_Mode.print_mode_active isabelle_processN;
 
 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
 
 val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
 
 
 (* restricted tracing messages *)
 
 val tracing_messages =
   Synchronized.var "tracing_messages" (Inttab.empty: int Inttab.table);
 
 fun reset_tracing exec_id =
   Synchronized.change tracing_messages (Inttab.delete_safe exec_id);
 
 fun update_tracing () =
   (case Position.parse_id (Position.thread_data ()) of
     NONE => ()
   | SOME exec_id =>
       let
         val ok =
           Synchronized.change_result tracing_messages (fn tab =>
             let
               val n = the_default 0 (Inttab.lookup tab exec_id) + 1;
               val limit = Options.default_int "editor_tracing_messages";
               val ok = limit <= 0 orelse n <= limit;
             in (ok, Inttab.update (exec_id, n) tab) end);
       in
         if ok then ()
         else
           let
             val (text, promise) = Active.dialog_text ();
             val _ =
               writeln ("Tracing paused.  " ^ text "Stop" ^ ", or continue with next " ^
                 text "100" ^ ", " ^ text "1000" ^ ", " ^ text "10000" ^ " messages?")
             val m = Value.parse_int (Future.join promise)
               handle Fail _ => error "Stopped";
           in
             Synchronized.change tracing_messages
               (Inttab.map_default (exec_id, 0) (fn k => k - m))
           end
       end);
 
 
 (* init protocol -- uninterruptible *)
 
 val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
 
 local
 
 fun recover crash =
   (Synchronized.change crashes (cons crash);
     Output.physical_stderr
       "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
 
 fun ml_statistics () =
   Output.protocol_message
     (Markup.ML_statistics {pid = ML_Pid.get (), stats_dir = getenv "POLYSTATSDIR"}) [];
 
 in
 
 fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
   let
     val _ = SHA1.test_samples ()
       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
 
     val _ = Output.physical_stderr Symbol.STX;
 
 
     (* streams *)
 
     val (in_stream, out_stream) = Socket_IO.open_streams address;
     val _ = Byte_Message.write_line out_stream (Bytes.string password);
 
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
     val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF);
 
 
     (* messages *)
 
     val message_channel = Message_Channel.make out_stream;
     val message = Message_Channel.message message_channel;
 
     fun standard_message props name ss =
       if forall (fn s => s = "") ss then ()
       else
         let
           val pos_props =
             if exists Markup.position_property props then props
             else props @ Position.properties_of (Position.thread_data ());
         in message name pos_props [XML.blob ss] end;
 
     fun report_message ss =
       if Context_Position.reports_enabled0 ()
       then standard_message [] Markup.reportN ss else ();
 
     val serial_props = Markup.serial_properties o serial;
 
     val message_context =
       Unsynchronized.setmp Private_Output.status_fn (standard_message [] Markup.statusN) #>
       Unsynchronized.setmp Private_Output.report_fn report_message #>
       Unsynchronized.setmp Private_Output.result_fn
         (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #>
       Unsynchronized.setmp Private_Output.writeln_fn
         (fn s => standard_message (serial_props ()) Markup.writelnN s) #>
       Unsynchronized.setmp Private_Output.state_fn
         (fn s => standard_message (serial_props ()) Markup.stateN s) #>
       Unsynchronized.setmp Private_Output.information_fn
         (fn s => standard_message (serial_props ()) Markup.informationN s) #>
       Unsynchronized.setmp Private_Output.tracing_fn
         (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #>
       Unsynchronized.setmp Private_Output.warning_fn
         (fn s => standard_message (serial_props ()) Markup.warningN s) #>
       Unsynchronized.setmp Private_Output.legacy_fn
         (fn s => standard_message (serial_props ()) Markup.legacyN s) #>
       Unsynchronized.setmp Private_Output.error_message_fn
         (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #>
       Unsynchronized.setmp Private_Output.system_message_fn
         (fn ss => message Markup.systemN [] [XML.blob ss]) #>
       Unsynchronized.setmp Private_Output.protocol_message_fn
         (fn props => fn chunks => message Markup.protocolN props chunks) #>
       Unsynchronized.setmp print_mode
         ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes));
 
 
     (* protocol *)
 
     fun protocol_loop () =
       let
         fun main () =
           (case Byte_Message.read_message in_stream of
             NONE => raise Protocol_Command.STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
           | SOME (name :: args) => Protocol_Command.run (Bytes.content name) args);
         val _ =
           (case Exn.capture_body main of
             Exn.Res () => ()
           | Exn.Exn exn =>
               if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
               else
                 (case Exn.capture Runtime.exn_system_message exn of
                   Exn.Res () => ()
                 | Exn.Exn crash => recover crash));
       in protocol_loop () end;
 
     fun protocol () =
      (message Markup.initN [] [[XML.Text (Session.welcome ())]];
       ml_statistics ();
       protocol_loop ());
 
     val result = Exn.capture_body (message_context protocol);
 
 
     (* shutdown *)
 
     val _ = Future.shutdown ();
     val _ = Execution.reset ();
     val _ = Message_Channel.shutdown message_channel;
     val _ = BinIO.closeIn in_stream;
     val _ = BinIO.closeOut out_stream;
 
     val _ = Options.reset_default ();
   in
     (case result of
       Exn.Exn (Protocol_Command.STOP rc) => if rc = 0 then () else exit rc
     | _ => Exn.release result)
   end);
 
 end;
 
 
 (* init options *)
 
 fun init_options () =
  (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Multithreading.parallel_proofs := Options.default_int "parallel_proofs";
   Isabelle_Thread.threads_stack_limit := Options.default_real "threads_stack_limit";
   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;
   Printer.show_markup_default := false;
   Context.theory_tracing := Options.default_bool "context_theory_tracing";
   Context.proof_tracing := Options.default_bool "context_proof_tracing";
-  Context.data_timing := Options.default_bool "context_data_timing");
+  Context.data_timing := Options.default_bool "context_data_timing";
+  Syntax.cache_persistent := false);
 
 fun init_options_interactive () =
  (init_options ();
   Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
-  Printer.show_markup_default := true);
+  Printer.show_markup_default := true;
+  Syntax.cache_persistent := true);
 
 
 (* generic init *)
 
 fun init_modes modes =
   let
     val address = Options.default_string \<^system_option>\<open>system_channel_address\<close>;
     val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
   in
     if address <> "" andalso password <> ""
     then init_protocol modes (address, password)
     else init_options ()
   end;
 
 fun init () = init_modes (protocol_modes1, protocol_modes2);
 fun init_build () = init_modes ([], protocol_modes2);
 
 end;
diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML
--- a/src/Pure/theory.ML
+++ b/src/Pure/theory.ML
@@ -1,396 +1,397 @@
 (*  Title:      Pure/theory.ML
     Author:     Lawrence C Paulson and Markus Wenzel
 
 Logical theory content: axioms, definitions, and begin/end wrappers.
 *)
 
 signature THEORY =
 sig
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val nodes_of: theory -> theory list
   val setup: (theory -> theory) -> unit
   val setup_result: (theory -> 'a * theory) -> 'a
   val local_setup: (Proof.context -> Proof.context) -> unit
   val local_setup_result: (Proof.context -> 'a * Proof.context) -> 'a
   val install_pure: theory -> unit
   val get_pure: unit -> theory
   val get_pure_bootstrap: unit -> theory
   val get_markup: theory -> Markup.T
   val check_theory: {get: string -> theory, all: unit -> string list} ->
     Proof.context -> string * Position.T -> theory
   val check: {long: bool} -> Proof.context -> string * Position.T -> theory
   val axiom_table: theory -> term Name_Space.table
   val axiom_space: theory -> Name_Space.T
   val all_axioms_of: theory -> (string * term) list
   val defs_of: theory -> Defs.T
   val at_begin: (theory -> theory option) -> theory -> theory
   val at_end: (theory -> theory option) -> theory -> theory
   val begin_theory: string * Position.T -> theory list -> theory
   val end_theory: theory -> theory
   val add_axiom: Proof.context -> binding * term -> theory -> theory
   val const_dep: theory -> string * typ -> Defs.entry
   val type_dep: string * typ list -> Defs.entry
   val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
   val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
   val add_deps_const: string -> theory -> theory
   val add_deps_type: string -> theory -> theory
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   val check_overloading: Proof.context -> bool -> string * typ -> unit
   val equality_axioms: (binding * term) list
 end
 
 structure Theory: THEORY =
 struct
 
 
 (** theory context operations **)
 
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;
 fun nodes_of thy = thy :: ancestors_of thy;
 
 fun setup f = Context.>> (Context.map_theory f);
 fun setup_result f = Context.>>> (Context.map_theory_result f);
 
 fun local_setup f = Context.>> (Context.map_proof f);
 fun local_setup_result f = Context.>>> (Context.map_proof_result f);
 
 
 (* implicit theory Pure *)
 
 val pure: theory Single_Assignment.var = Single_Assignment.var "pure";
 
 fun install_pure thy = Single_Assignment.assign pure thy;
 
 fun get_pure () =
   (case Single_Assignment.peek pure of
     SOME thy => thy
   | NONE => raise Fail "Theory Pure not present");
 
 fun get_pure_bootstrap () =
   (case Single_Assignment.peek pure of
     SOME thy => thy
   | NONE => Context.the_global_context ());
 
 
 
 (** datatype thy **)
 
 type wrapper = (theory -> theory option) * stamp;
 
 fun apply_wrappers (wrappers: wrapper list) =
   perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
 
 datatype thy = Thy of
  {pos: Position.T,
   id: serial,
   axioms: term Name_Space.table,
   defs: Defs.T,
   wrappers: wrapper list * wrapper list};
 
 fun rep_thy (Thy args) = args;
 
 fun make_thy (pos, id, axioms, defs, wrappers) =
   Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
 
 structure Thy = Theory_Data'
 (
   type T = thy;
   val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
   fun merge args =
     let
       val thy0 = #1 (hd args);
       val {pos, id, ...} = rep_thy (#2 (hd args));
 
       val merge_defs = Defs.merge (Defs.global_context thy0);
       val merge_wrappers = Library.merge (eq_snd op =);
 
       val axioms' = Library.foldl1 Name_Space.merge_tables (map (#axioms o rep_thy o #2) args);
       val defs' = Library.foldl1 merge_defs (map (#defs o rep_thy o #2) args);
       val bgs' = Library.foldl1 merge_wrappers (map (#1 o #wrappers o rep_thy o #2) args);
       val ens' = Library.foldl1 merge_wrappers (map (#2 o #wrappers o rep_thy o #2) args);
     in make_thy (pos, id, axioms', defs', (bgs', ens')) end;
 );
 
 val rep_theory = rep_thy o Thy.get;
 
 fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
   make_thy (f (pos, id, axioms, defs, wrappers)));
 
 fun map_axioms f =
   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
 
 fun map_defs f =
   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
 
 fun map_wrappers f =
   map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
 
 
 (* entity markup *)
 
 fun theory_markup def name id pos =
   if id = 0 then Markup.empty
   else Position.make_entity_markup def id Markup.theoryN (name, pos);
 
 fun init_markup (name, pos) thy =
   let
     val id = serial ();
     val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)];
   in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
 
 fun get_markup thy =
   let val {pos, id, ...} = rep_theory thy
   in theory_markup {def = false} (Context.theory_long_name thy) id pos end;
 
 fun check_theory {get, all} ctxt (name, pos) =
   let
     val thy = get name handle ERROR msg =>
       let
         val completion_report =
           Completion.make_report (name, pos)
             (fn completed =>
               all ()
               |> filter (completed o Long_Name.base_name)
               |> sort_strings
               |> map (fn a => (a, (Markup.theoryN, a))));
       in error (msg ^ Position.here pos ^ completion_report) end;
     val _ = Context_Position.report ctxt pos (get_markup thy);
   in thy end;
 
 fun check long ctxt arg =
   let
     val thy = Proof_Context.theory_of ctxt;
     val get = Context.get_theory long thy;
     fun all () = map (Context.theory_name long) (ancestors_of thy);
   in check_theory {get = get, all = all} ctxt arg end;
 
 
 (* basic operations *)
 
 val axiom_table = #axioms o rep_theory;
 val axiom_space = Name_Space.space_of_table o axiom_table;
 
 val all_axioms_of = Name_Space.dest_table o axiom_table;
 
 val defs_of = #defs o rep_theory;
 
 
 (* begin/end theory *)
 
 val begin_wrappers = rev o #1 o #wrappers o rep_theory;
 val end_wrappers = rev o #2 o #wrappers o rep_theory;
 
 fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
 fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
 
 fun begin_theory (name, pos) imports =
   if name = Context.PureN then
     (case imports of
       [thy] => init_markup (name, pos) thy
     | _ => error "Bad bootstrapping of theory Pure")
   else
     let
       val thy = Context.begin_thy name imports;
       val wrappers = begin_wrappers thy;
     in
       thy
       |> init_markup (name, pos)
       |> Sign.init_naming
       |> Sign.local_path
       |> apply_wrappers wrappers
+      |> tap (Syntax.cache_syntax o Sign.syn_of)
     end;
 
 fun end_theory thy =
   thy
   |> apply_wrappers (end_wrappers thy)
   |> Sign.change_check
   |> Context.finish_thy;
 
 
 
 (** primitive specifications **)
 
 (* raw axioms *)
 
 fun cert_axm ctxt (b, raw_tm) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val t = Sign.cert_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
     val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
 
     val bad_sorts =
       rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
     val _ = null bad_sorts orelse
       error ("Illegal sort constraints in primitive specification: " ^
         commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
   in (b, Sign.no_vars ctxt t) end
   handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
 
 fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   let
     val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
     val context = ctxt
       |> Sign.inherit_naming thy
       |> Context_Position.set_visible_generic false;
     val (_, axioms') = Name_Space.define context true axm axioms;
   in axioms' end);
 
 
 (* dependencies *)
 
 fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
 fun type_dep (c, args) = ((Defs.Type, c), args);
 
 fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
   let
     fun prep (item, args) =
       (case fold Term.add_tvarsT args [] of
         [] => (item, map Logic.varifyT_global args)
       | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, []));
 
     val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs));
     val rhs_extras =
       TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd))
       |> TFrees.keys;
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote description);
   in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
 
 fun cert_entry thy ((Defs.Const, c), args) =
       Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
       |> dest_Const |> const_dep thy
   | cert_entry thy ((Defs.Type, c), args) =
       Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
 
 fun add_deps context a raw_lhs raw_rhs thy =
   let
     val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
     val description = if a = "" then lhs_name ^ " axiom" else a;
   in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
 
 fun add_deps_global a x y thy =
   add_deps (Defs.global_context thy) a x y thy;
 
 fun add_deps_const c thy =
   let val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
   in thy |> add_deps_global "" (const_dep thy (c, T)) [] end;
 
 fun add_deps_type c thy =
   let
     val n = Sign.arity_number thy c;
     val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
   in thy |> add_deps_global "" (type_dep (c, args)) [] end
 
 fun specify_const decl thy =
   let val (t, thy') = Sign.declare_const_global decl thy;
   in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
 
 
 (* overloading *)
 
 fun check_overloading ctxt overloaded (c, T) =
   let
     val thy = Proof_Context.theory_of ctxt;
 
     val declT = Sign.the_const_constraint thy c
       handle TYPE (msg, _, _) => error msg;
     val T' = Logic.varifyT_global T;
 
     fun message sorts txt =
       [Pretty.block [Pretty.str "Specification of constant ",
         Pretty.str c, Pretty.str " ::", Pretty.brk 1,
         Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   in
     if Sign.typ_instance thy (declT, T') then ()
     else if Type.raw_instance (declT, T') then
       error (message true "imposes additional sort constraints on the constant declaration")
     else if overloaded then ()
     else
       error (message false "is strictly less general than the declared type (overloading required)")
   end;
 
 
 (* definitional axioms *)
 
 local
 
 fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
   let
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _, _) =
       Primitive_Defs.dest_def ctxt
         {check_head = Term.is_Const,
          check_free_lhs = K true,
          check_free_rhs = K false,
          check_tfree = K false} tm
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);
 
     val rhs_consts =
       fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs [];
     val rhs_types =
       (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs [];
     val rhs_deps = rhs_consts @ rhs_types;
 
     val _ = check_overloading ctxt overloaded lhs_const;
   in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
 
 in
 
 fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
   let val axm = cert_axm ctxt raw_axm in
     thy
     |> map_defs (check_def context thy unchecked overloaded axm)
     |> add_axiom ctxt axm
   end;
 
 end;
 
 
 (** axioms for equality **)
 
 local
 
 val aT = TFree ("'a", []);
 val bT = TFree ("'b", []);
 val x = Free ("x", aT);
 val y = Free ("y", aT);
 val z = Free ("z", aT);
 val A = Free ("A", propT);
 val B = Free ("B", propT);
 val f = Free ("f", aT --> bT);
 val g = Free ("g", aT --> bT);
 
 in
 
 val equality_axioms =
  [(Binding.make ("reflexive", \<^here>), Logic.mk_equals (x, x)),
   (Binding.make ("symmetric", \<^here>),
     Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
   (Binding.make ("transitive", \<^here>),
     Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
   (Binding.make ("equal_intr", \<^here>),
     Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
   (Binding.make ("equal_elim", \<^here>), Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
   (Binding.make ("abstract_rule", \<^here>),
     Logic.mk_implies
       (Logic.all x (Logic.mk_equals (f $ x, g $ x)),
         Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
   (Binding.make ("combination", \<^here>), Logic.list_implies
     ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
 
 end;
 
 end;