diff --git a/src/Pure/Build/export_theory.ML b/src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML
+++ b/src/Pure/Build/export_theory.ML
@@ -1,479 +1,479 @@
 (*  Title:      Pure/Build/export_theory.ML
     Author:     Makarius
 
 Export foundational theory content and locale/class structure.
 *)
 
 signature EXPORT_THEORY =
 sig
   val other_name_space: (theory -> Name_Space.T) -> theory -> theory
   val export_enabled: Thy_Info.presentation_context -> bool
   val export_body: theory -> string -> XML.body -> unit
 end;
 
 structure Export_Theory: EXPORT_THEORY =
 struct
 
 (* other name spaces *)
 
 fun err_dup_kind kind = error ("Duplicate name space kind " ^ quote kind);
 
 structure Data = Theory_Data
 (
   type T = (theory -> Name_Space.T) Inttab.table;
   val empty = Inttab.empty;
   val merge = Inttab.merge (K true);
 );
 
 val other_name_spaces = map #2 o Inttab.dest o Data.get;
 fun other_name_space get_space thy = Data.map (Inttab.update (serial (), get_space)) thy;
 
 val _ = Theory.setup
  (other_name_space Thm.oracle_space #>
   other_name_space Global_Theory.fact_space #>
   other_name_space (Bundle.bundle_space o Context.Theory) #>
   other_name_space (Attrib.attribute_space o Context.Theory) #>
   other_name_space (Method.method_space o Context.Theory));
 
 
 (* approximative syntax *)
 
-val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
+val get_syntax = Syntax.get_approx o Proof_Context.syntax_of;
 fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type;
 fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const;
 fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed;
 
 fun get_syntax_param ctxt loc x =
   let val thy = Proof_Context.theory_of ctxt in
     if Class.is_class thy loc then
       (case AList.lookup (op =) (Class.these_params thy [loc]) x of
         NONE => NONE
       | SOME (_, (c, _)) => get_syntax_const ctxt c)
     else get_syntax_fixed ctxt x
   end;
 
 val encode_syntax =
   XML.Encode.variant
    [fn NONE => ([], []),
     fn SOME (Syntax.Prefix delim) => ([delim], []),
     fn SOME (Syntax.Infix {assoc, delim, pri}) =>
       let
         val ass =
           (case assoc of
             Printer.No_Assoc => 0
           | Printer.Left_Assoc => 1
           | Printer.Right_Assoc => 2);
         open XML.Encode Term_XML.Encode;
       in ([], triple int string int (ass, delim, pri)) end];
 
 
 (* free variables: not declared in the context *)
 
 val is_free = not oo Name.is_declared;
 
 fun add_frees used =
   fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I);
 
 fun add_tfrees used =
   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
 
 
 (* locales *)
 
 fun locale_content thy loc =
   let
     val ctxt = Locale.init loc thy;
     val args =
       Locale.params_of thy loc
       |> map (fn ((x, T), _) => ((x, T), get_syntax_param ctxt loc x));
     val axioms =
       let
         val (asm, defs) = Locale.specification_of thy loc;
         val cprops = map (Thm.cterm_of ctxt) (the_list asm @ defs);
         val (intro1, intro2) = Locale.intros_of thy loc;
         val intros_tac = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2) [];
         val res =
           Goal.init (Conjunction.mk_conjunction_balanced cprops)
           |> (ALLGOALS Goal.conjunction_tac THEN intros_tac)
           |> try Seq.hd;
       in
         (case res of
           SOME goal => Thm.prems_of goal
         | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
       end;
     val typargs = build_rev (fold Term.add_tfrees (map (Free o #1) args @ axioms));
   in {typargs = typargs, args = args, axioms = axioms} end;
 
 fun get_locales thy =
   Locale.get_locales thy |> map_filter (fn loc =>
     if Experiment.is_experiment thy loc then NONE else SOME (loc, ()));
 
 fun get_dependencies prev_thys thy =
   Locale.dest_dependencies prev_thys thy |> map_filter (fn dep =>
     if Experiment.is_experiment thy (#source dep) orelse
       Experiment.is_experiment thy (#target dep) then NONE
     else
       let
         val (type_params, params) = Locale.parameters_of thy (#source dep);
         val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
         val substT =
           typargs |> map_filter (fn v =>
             let
               val T = TFree v;
               val T' = Morphism.typ (#morphism dep) T;
             in if T = T' then NONE else SOME (v, T') end);
         val subst =
           params |> map_filter (fn (v, _) =>
             let
               val t = Free v;
               val t' = Morphism.term (#morphism dep) t;
             in if t aconv t' then NONE else SOME (v, t') end);
       in SOME (dep, (substT, subst)) end);
 
 
 (* presentation *)
 
 fun export_enabled (context: Thy_Info.presentation_context) =
   Options.bool (#options context) "export_theory";
 
 fun export_body thy name body =
   if XML.is_empty_body body then ()
   else Export.export thy (Path.binding0 (Path.make ("theory" :: space_explode "/" name))) body;
 
 val _ = (Theory.setup o Thy_Info.add_presentation) (fn context => fn thy =>
   let
     val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     val consts = Sign.consts_of thy;
     val thy_ctxt = Proof_Context.init_global thy;
 
     val pos_properties = Thy_Info.adjust_pos_properties context;
 
     val enabled = export_enabled context;
 
 
     (* strict parents *)
 
     val parents = Theory.parents_of thy;
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
         (XML.Encode.string (cat_lines (map Context.theory_long_name parents) ^ "\n"));
 
 
     (* spec rules *)
 
     fun spec_rule_content {pos, name, rough_classification, terms, rules} =
       let
         val spec =
           terms @ map Thm.plain_prop_of rules
           |> Term_Subst.zero_var_indexes_list
           |> map Logic.unvarify_global;
       in
        {props = pos_properties pos,
         name = name,
         rough_classification = rough_classification,
         typargs = build_rev (fold Term.add_tfrees spec),
         args = build_rev (fold Term.add_frees spec),
         terms = map (fn t => (t, Term.type_of t)) (take (length terms) spec),
         rules = drop (length terms) spec}
       end;
 
 
     (* entities *)
 
     fun make_entity_markup name xname pos serial =
       let val props = pos_properties pos @ Markup.serial_properties serial;
       in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
 
     fun entity_markup space name =
       let
         val xname = Name_Space.extern_shortest thy_ctxt space name;
         val {serial, pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup name xname pos serial end;
 
     fun export_entities export_name get_space decls export =
       let
         val parent_spaces = map get_space parents;
         val space = get_space thy;
       in
         build (decls |> fold (fn (name, decl) =>
           if exists (fn space => Name_Space.declared space name) parent_spaces then I
           else
             (case export name decl of
               NONE => I
             | SOME make_body =>
                 let
                   val i = #serial (Name_Space.the_entry space name);
                   val body = if enabled then make_body () else [];
                 in cons (i, XML.Elem (entity_markup space name, body)) end)))
         |> sort (int_ord o apply2 #1) |> map #2
         |> export_body thy export_name
       end;
 
 
     (* types *)
 
     val encode_type =
       let open XML.Encode Term_XML.Encode
       in triple encode_syntax (list string) (option typ) end;
 
     val _ =
       export_entities "types" Sign.type_space (Name_Space.dest_table (#types rep_tsig))
         (fn c =>
           (fn Type.Logical_Type n =>
                 SOME (fn () =>
                   encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
             | Type.Abbreviation (args, U, false) =>
                 SOME (fn () =>
                   encode_type (get_syntax_type thy_ctxt c, args, SOME U))
             | _ => NONE));
 
 
     (* consts *)
 
     val encode_term = Term_XML.Encode.term consts;
 
     val encode_const =
       let open XML.Encode Term_XML.Encode
       in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end;
 
     val _ =
       export_entities "consts" Sign.const_space (#constants (Consts.dest consts))
         (fn c => fn (T, abbrev) =>
           SOME (fn () =>
             let
               val syntax = get_syntax_const thy_ctxt c;
               val U = Logic.unvarifyT_global T;
               val U0 = Term.strip_sortsT U;
               val trim_abbrev = Proofterm.standard_vars_term Name.context #> Term.strip_sorts;
               val abbrev' = Option.map trim_abbrev abbrev;
               val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
               val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
             in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end));
 
 
     (* axioms *)
 
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
         val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
         val args = rev (add_frees used prop []);
         val typargs = rev (add_tfrees used prop []);
         val used_typargs = fold (Name.declare o #1) typargs used;
         val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
       in ((sorts @ typargs, args, prop), proof) end;
 
     fun standard_prop_of thm =
       standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
 
     val encode_prop =
       let open XML.Encode Term_XML.Encode
       in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
 
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
 
     val _ =
       export_entities "axioms" Theory.axiom_space (Theory.all_axioms_of thy)
         (fn _ => fn prop => SOME (fn () => encode_axiom Name.context prop));
 
 
     (* theorems and proof terms *)
 
     val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
     val prep_thm = clean_thm #> Thm.unconstrainT #> Thm.strip_shyps;
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
       if #serial header = #serial thm_id then ""
       else
         (case lookup_thm_id (Proofterm.thm_header_id header) of
           NONE => ""
         | SOME thm_name => Thm_Name.print thm_name);
 
     fun entity_markup_thm (serial, (name, i)) =
       let
         val space = Global_Theory.fact_space thy;
         val xname = Name_Space.extern_shortest thy_ctxt space name;
         val {pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
 
     fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = prep_thm raw_thm;
 
         val proof0 =
           if Proofterm.export_standard_enabled () then
             Proof_Syntax.standard_proof_of
               {full = true, expand_name = SOME o expand_name thm_id} thm
           else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
           else MinProof;
         val (prop, SOME proof) = standard_prop_of thm (SOME proof0);
         val _ = Thm.expose_proofs thy [thm];
       in
         (prop, deps, proof) |>
           let
             open XML.Encode Term_XML.Encode;
             val encode_proof = Proofterm.encode_standard_proof consts;
           in triple encode_prop (list string) encode_proof end
       end;
 
     fun export_thm (thm_id, thm_name) =
       let
         val markup = entity_markup_thm (#serial thm_id, thm_name);
         val body =
           if enabled then
             Global_Theory.get_thm_name thy (thm_name, Position.none)
             |> encode_thm thm_id
           else [];
       in XML.Elem (markup, body) end;
 
     val _ = export_body thy "thms" (map export_thm (Global_Theory.dest_thm_names thy));
 
 
     (* type classes *)
 
     val encode_class =
       let open XML.Encode Term_XML.Encode
       in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
 
     val _ =
       export_entities "classes" Sign.class_space
         (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))))
         (fn name => fn () => SOME (fn () =>
           (case try (Axclass.get_info thy) name of
             NONE => ([], [])
           | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
           |> encode_class));
 
 
     (* sort algebra *)
 
     val _ =
       if enabled then
         let
           val prop = encode_axiom Name.context o Logic.varify_global;
 
           val encode_classrel =
             let open XML.Encode
             in list (pair prop (pair string string)) end;
 
           val encode_arities =
             let open XML.Encode Term_XML.Encode
             in list (pair prop (triple string (list sort) string)) end;
 
           val export_classrel =
             maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
 
           val export_arities = map (`Logic.mk_arity) #> encode_arities;
 
           val {classrel, arities} =
             Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
               (#2 (#classes rep_tsig));
         in
           if null classrel then () else export_body thy "classrel" (export_classrel classrel);
           if null arities then () else export_body thy "arities" (export_arities arities)
         end
       else ();
 
 
     (* locales *)
 
     fun encode_locale used =
       let open XML.Encode Term_XML.Encode in
         triple (list (pair string sort)) (list (pair (pair string typ) encode_syntax))
           (list (encode_axiom used))
       end;
 
     val _ =
       export_entities "locales" Locale.locale_space (get_locales thy)
         (fn loc => fn () => SOME (fn () =>
           let
             val {typargs, args, axioms} = locale_content thy loc;
             val used = fold Name.declare (map #1 typargs @ map (#1 o #1) args) Name.context;
           in encode_locale used (typargs, args, axioms) end
           handle ERROR msg =>
             cat_error msg ("The error(s) above occurred in locale " ^
               quote (Locale.markup_name thy_ctxt loc))));
 
 
     (* locale dependencies *)
 
     fun encode_locale_dependency (dep: Locale.locale_dependency, subst) =
       (#source dep, (#target dep, (#prefix dep, subst))) |>
         let
           open XML.Encode Term_XML.Encode;
           val encode_subst =
             pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) (term consts)));
         in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
 
     val _ =
       if enabled then
         get_dependencies parents thy |> map_index (fn (i, dep) =>
           let
             val xname = string_of_int (i + 1);
             val name = Long_Name.implode [Context.theory_base_name thy, xname];
             val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
             val body = encode_locale_dependency dep;
           in XML.Elem (markup, body) end)
         |> export_body thy "locale_dependencies"
       else ();
 
 
     (* constdefs *)
 
     val _ =
       if enabled then
         let
           val constdefs =
             Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy)
             |> sort_by #1;
           val encode =
             let open XML.Encode
             in list (pair string string) end;
         in if null constdefs then () else export_body thy "constdefs" (encode constdefs) end
       else ();
 
 
     (* spec rules *)
 
     val encode_specs =
       let open XML.Encode Term_XML.Encode in
         list (fn {props, name, rough_classification, typargs, args, terms, rules} =>
           pair properties (pair string (pair Spec_Rules.encode_rough_classification
             (pair (list (pair string sort)) (pair (list (pair string typ))
               (pair (list (pair encode_term typ)) (list encode_term))))))
               (props, (name, (rough_classification, (typargs, (args, (terms, rules)))))))
       end;
 
     val _ =
       if enabled then
         (case Spec_Rules.dest_theory thy of
           [] => ()
         | spec_rules =>
             export_body thy "spec_rules" (encode_specs (map spec_rule_content spec_rules)))
       else ();
 
 
     (* other entities *)
 
     fun export_other get_space =
       let
         val space = get_space thy;
         val export_name = "other/" ^ Name_Space.kind_of space;
         val decls = Name_Space.get_names space |> map (rpair ());
       in export_entities export_name get_space decls (fn _ => fn () => SOME (K [])) end;
 
     val other_spaces = other_name_spaces thy;
     val other_kinds = map (fn get_space => Name_Space.kind_of (get_space thy)) other_spaces;
     val _ =
       if null other_kinds then ()
       else
         Export.export thy \<^path_binding>\<open>theory/other_kinds\<close>
           (XML.Encode.string (cat_lines other_kinds));
     val _ = List.app export_other other_spaces;
 
   in () end);
 
 end;
diff --git a/src/Pure/Isar/proof_context.ML b/src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML
+++ b/src/Pure/Isar/proof_context.ML
@@ -1,1669 +1,1668 @@
 (*  Title:      Pure/Isar/proof_context.ML
     Author:     Markus Wenzel, TU Muenchen
 
 The key concept of Isar proof contexts: elevates primitive local
 reasoning Gamma |- phi to a structured concept, with generic context
 elements.  See also structure Variable and Assumption.
 *)
 
 signature PROOF_CONTEXT =
 sig
   val theory_of: Proof.context -> theory
   val init_global: theory -> Proof.context
   val get_global: {long: bool} -> theory -> string -> Proof.context
   type mode
   val mode_default: mode
   val mode_pattern: mode
   val mode_schematic: mode
   val mode_abbrev: mode
   val set_mode: mode -> Proof.context -> Proof.context
   val get_mode: Proof.context -> mode
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
-  val syn_of: Proof.context -> Syntax.syntax
+  val syntax_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
   val arity_sorts: Proof.context -> string -> sort -> sort list
   val consts_of: Proof.context -> Consts.T
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
   val get_scope: Proof.context -> Binding.scope option
   val new_scope: Proof.context -> Binding.scope * Proof.context
   val private_scope: Binding.scope -> Proof.context -> Proof.context
   val private: Position.T -> Proof.context -> Proof.context
   val qualified_scope: Binding.scope -> Proof.context -> Proof.context
   val qualified: Position.T -> Proof.context -> Proof.context
   val concealed: Proof.context -> Proof.context
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
   val const_space: Proof.context -> Name_Space.T
   val defs_context: Proof.context -> Defs.context
   val intern_class: Proof.context -> xstring -> string
   val intern_type: Proof.context -> xstring -> string
   val intern_const: Proof.context -> xstring -> string
   val extern_class: Proof.context -> string -> xstring
   val markup_class: Proof.context -> string -> string
   val pretty_class: Proof.context -> string -> Pretty.T
   val extern_type: Proof.context -> string -> xstring
   val markup_type: Proof.context -> string -> string
   val pretty_type: Proof.context -> string -> Pretty.T
   val extern_const: Proof.context -> string -> xstring
   val markup_const: Proof.context -> string -> string
   val pretty_const: Proof.context -> string -> Pretty.T
   val transfer: theory -> Proof.context -> Proof.context
   val transfer_facts: theory -> Proof.context -> Proof.context
   val background_theory: (theory -> theory) -> Proof.context -> Proof.context
   val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val facts_of: Proof.context -> Facts.T
   val facts_of_fact: Proof.context -> string -> Facts.T
   val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring
   val augment: term -> Proof.context -> Proof.context
   val print_name: Proof.context -> string -> string
   val pretty_name: Proof.context -> string -> Pretty.T
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
   val read_class: Proof.context -> string -> class
   val read_typ: Proof.context -> string -> typ
   val read_typ_syntax: Proof.context -> string -> typ
   val read_typ_abbrev: Proof.context -> string -> typ
   val cert_typ: Proof.context -> typ -> typ
   val cert_typ_syntax: Proof.context -> typ -> typ
   val cert_typ_abbrev: Proof.context -> typ -> typ
   val infer_type: Proof.context -> string * typ -> typ
   val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
   val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
   val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T -> typ * Position.report list
   val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ
   val consts_completion_message: Proof.context -> xstring * Position.T list -> string
   val check_const: {proper: bool, strict: bool} -> Proof.context ->
     xstring * Position.T list -> term * Position.report list
   val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term
   val read_arity: Proof.context -> xstring * string list * string -> arity
   val cert_arity: Proof.context -> arity -> arity
   val allow_dummies: Proof.context -> Proof.context
   val prepare_sortsT: Proof.context -> typ list -> string list * typ list
   val prepare_sorts: Proof.context -> term list -> string list * term list
   val check_tfree: Proof.context -> string * sort -> string * sort
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
   val show_abbrevs: bool Config.T
   val expand_abbrevs: Proof.context -> term -> term
   val cert_term: Proof.context -> term -> term
   val cert_prop: Proof.context -> term -> term
   val def_type: Proof.context -> indexname -> typ option
   val standard_typ_check: Proof.context -> typ list -> typ list
   val standard_term_check_finish: Proof.context -> term list -> term list
   val standard_term_uncheck: Proof.context -> term list -> term list
   val export_: {goal: bool} -> Proof.context -> Proof.context -> thm list -> thm list
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_goal: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val auto_bind_goal: term list -> Proof.context -> Proof.context
   val auto_bind_facts: term list -> Proof.context -> Proof.context
   val simult_matches: Proof.context -> term * term list -> (indexname * term) list
   val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
   val bind_term: indexname * term -> Proof.context -> Proof.context
   val cert_propp: Proof.context -> (term * term list) list list ->
     (term list list * (indexname * term) list)
   val read_propp: Proof.context -> (string * string list) list list ->
     (term list list * (indexname * term) list)
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
   val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option
   val dynamic_facts_dummy: bool Config.T
   val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
   val is_stmt: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
   val restore_stmt: Proof.context -> Proof.context -> Proof.context
   val add_thms_dynamic: binding * (Context.generic -> thm list) ->
     Proof.context -> string * Proof.context
   val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context
   val note_thms: string -> Thm.binding * (thm list * attribute list) list ->
     Proof.context -> (string * thm list) * Proof.context
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   val alias_fact: binding -> string -> Proof.context -> Proof.context
   val read_var: binding * string option * mixfix -> Proof.context ->
     (binding * typ option * mixfix) * Proof.context
   val cert_var: binding * typ option * mixfix -> Proof.context ->
     (binding * typ option * mixfix) * Proof.context
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val add_assms: Assumption.export ->
     (Thm.binding * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_assms_cmd: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list
   val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   val check_case: Proof.context -> bool ->
     string * Position.T -> binding option list -> Rule_Cases.T
   val check_syntax_const: Proof.context -> string * Position.T -> string
   val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
     Proof.context -> Proof.context
   val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
     Context.generic -> Context.generic
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val type_alias: binding -> string -> Proof.context -> Proof.context
   val const_alias: binding -> string -> Proof.context -> Proof.context
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val generic_add_abbrev: string -> binding * term -> Context.generic ->
     (term * term) * Context.generic
   val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   type stmt =
    {vars: ((binding * typ option * mixfix) * (string * term)) list,
     propss: term list list,
     binds: (indexname * term) list,
     result_binds: (indexname * term) list}
   val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list ->
     Proof.context -> stmt * Proof.context
   val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list ->
     Proof.context -> stmt * Proof.context
   type statement =
    {fixes: (string * term) list,
     assumes: term list list,
     shows: term list list,
     result_binds: (indexname * term option) list,
     text: term,
     result_text: term}
   val cert_statement: (binding * typ option * mixfix) list ->
     (term * term list) list list -> (term * term list) list list -> Proof.context ->
     statement * Proof.context
   val read_statement: (binding * string option * mixfix) list ->
     (string * string list) list list -> (string * string list) list list -> Proof.context ->
     statement * Proof.context
   val print_syntax: Proof.context -> unit
   val print_abbrevs: bool -> Proof.context -> unit
   val pretty_term_bindings: Proof.context -> Pretty.T list
   val pretty_local_facts: bool -> Proof.context -> Pretty.T list
   val print_local_facts: bool -> Proof.context -> unit
   val pretty_cases: Proof.context -> Pretty.T list
   val print_cases_proof: Proof.context -> Proof.context -> string
   val debug: bool Config.T
   val verbose: bool Config.T
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
 end;
 
 structure Proof_Context: PROOF_CONTEXT =
 struct
 
 val theory_of = Proof_Context.theory_of;
 val init_global = Proof_Context.init_global;
 val get_global = Proof_Context.get_global;
 
 
 
 (** inner syntax mode **)
 
 datatype mode =
   Mode of
    {pattern: bool,             (*pattern binding schematic variables*)
     schematic: bool,           (*term referencing loose schematic variables*)
     abbrev: bool};             (*abbrev mode -- no normalization*)
 
 fun make_mode (pattern, schematic, abbrev) =
   Mode {pattern = pattern, schematic = schematic, abbrev = abbrev};
 
 val mode_default   = make_mode (false, false, false);
 val mode_pattern   = make_mode (true, false, false);
 val mode_schematic = make_mode (false, true, false);
 val mode_abbrev    = make_mode (false, false, true);
 
 
 
 (** Isar proof context information **)
 
 type cases = Rule_Cases.T Name_Space.table;
 val empty_cases: cases = Name_Space.empty_table Markup.caseN;
 
 datatype data =
   Data of
    {mode: mode,                  (*inner syntax mode*)
     syntax: Local_Syntax.T,      (*local syntax*)
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
     facts: Facts.T,              (*local facts, based on initial global facts*)
     cases: cases};               (*named case contexts*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
   Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
 
 structure Data = Proof_Data
 (
   type T = data;
   fun init thy =
     make_data (mode_default,
       Local_Syntax.init thy,
       (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy),
       (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy),
       Global_Theory.facts_of thy,
       empty_cases);
 );
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
 fun map_data_result f ctxt =
   let
     val Data {mode, syntax, tsig, consts, facts, cases} = Data.get ctxt;
     val (res, data') = f (mode, syntax, tsig, consts, facts, cases) ||> make_data;
   in (res, Data.put data' ctxt) end;
 
 fun map_data f = snd o map_data_result (pair () o f);
 
 fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
   (mode, syntax, tsig, consts, facts, cases));
 
 fun map_syntax f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, f syntax, tsig, consts, facts, cases));
 
 fun map_syntax_idents f ctxt =
   let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in
     ctxt
     |> map_syntax (K syntax')
     |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents')
   end;
 
 fun map_tsig f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, f tsig, consts, facts, cases));
 
 fun map_consts f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, tsig, f consts, facts, cases));
 
 fun map_facts_result f =
   map_data_result (fn (mode, syntax, tsig, consts, facts, cases) =>
     let val (res, facts') = f facts
     in (res, (mode, syntax, tsig, consts, facts', cases)) end);
 
 fun map_facts f = snd o map_facts_result (pair () o f);
 
 fun map_cases f =
   map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
     (mode, syntax, tsig, consts, facts, f cases));
 
 val get_mode = #mode o rep_data;
 val restore_mode = set_mode o get_mode;
 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
 
-val syntax_of = #syntax o rep_data;
-val syn_of = Local_Syntax.syn_of o syntax_of;
+val syntax_of = Local_Syntax.syntax_of o #syntax o rep_data;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
-val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
+val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o #syntax o rep_data;
 
 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
 
 val consts_of = #1 o #consts o rep_data;
 val cases_of = #cases o rep_data;
 
 
 (* naming *)
 
 val naming_of = Name_Space.naming_of o Context.Proof;
 val map_naming = Context.proof_map o Name_Space.map_naming;
 val restore_naming = map_naming o K o naming_of;
 
 val full_name = Name_Space.full_name o naming_of;
 
 val get_scope = Name_Space.get_scope o naming_of;
 
 fun new_scope ctxt =
   let
     val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
     val ctxt' = map_naming (K naming') ctxt;
   in (scope, ctxt') end;
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
 val qualified_scope = map_naming o Name_Space.qualified_scope;
 val qualified = map_naming o Name_Space.qualified;
 
 val concealed = map_naming Name_Space.concealed;
 
 
 (* name spaces *)
 
 val class_space = Type.class_space o tsig_of;
 val type_space = Type.type_space o tsig_of;
 val const_space = Consts.space_of o consts_of;
 
 fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt));
 
 val intern_class = Name_Space.intern o class_space;
 val intern_type = Name_Space.intern o type_space;
 val intern_const = Name_Space.intern o const_space;
 
 fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
 fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
 fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
 
 fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup;
 fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup;
 fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup;
 
 fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str;
 fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str;
 fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str;
 
 
 (* theory transfer *)
 
 fun transfer_syntax thy ctxt = ctxt |>
   map_syntax (Local_Syntax.rebuild thy) |>
   map_tsig (fn tsig as (local_tsig, global_tsig) =>
     let val thy_tsig = Sign.tsig_of thy in
       if Type.eq_tsig (thy_tsig, global_tsig) then tsig
       else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
       if Consts.eq_consts (thy_consts, global_consts) then consts
       else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
     end);
 
 fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
 
 fun transfer_facts thy =
   map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts));
 
 fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
 
 fun background_theory_result f ctxt =
   let val (res, thy') = f (theory_of ctxt)
   in (res, ctxt |> transfer thy') end;
 
 
 (* hybrid facts *)
 
 val facts_of = #facts o rep_data;
 
 fun facts_of_fact ctxt name =
   let
     val local_facts = facts_of ctxt;
     val global_facts = Global_Theory.facts_of (theory_of ctxt);
   in
     if Facts.defined local_facts name
     then local_facts else global_facts
   end;
 
 fun markup_extern_fact ctxt name =
   let
     val facts = facts_of_fact ctxt name;
     val (markup, xname) = Facts.markup_extern ctxt facts name;
     val markups =
       if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name]
       else [markup];
   in (markups, xname) end;
 
 
 (* augment context by implicit term declarations *)
 
 fun augment t ctxt = ctxt
   |> Variable.add_fixes_implicit t
   |> Variable.declare_term t
   |> Soft_Type_System.augment t;
 
 
 
 (** pretty printing **)
 
 val print_name = Token.print_name o Thy_Header.get_keywords';
 val pretty_name = Pretty.str oo print_name;
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
 fun pretty_fact_name ctxt a =
   Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"];
 
 fun pretty_fact ctxt =
   let
     val pretty_thm = Thm.pretty_thm ctxt;
     val pretty_thms = map (Thm.pretty_thm_item ctxt);
   in
     fn ("", [th]) => pretty_thm th
      | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
      | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th]
      | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths))
   end;
 
 
 
 (** prepare types **)
 
 (* classes *)
 
 fun check_class ctxt (xname, pos) =
   let
     val tsig = tsig_of ctxt;
     val class_space = Type.class_space tsig;
 
     val name = Type.cert_class tsig (Name_Space.intern class_space xname)
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
           Completion.markup_report
             [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]);
     val reports =
       if Context_Position.is_reported ctxt pos
       then [(pos, Name_Space.markup class_space name)] else [];
   in (name, reports) end;
 
 fun read_class ctxt text =
   let
     val source = Syntax.read_input text;
     val (c, reports) = check_class ctxt (Input.source_content source);
     val _ = Context_Position.reports ctxt reports;
   in c end;
 
 
 (* types *)
 
 fun read_typ_mode mode ctxt s =
   Syntax.read_typ (Type.set_mode mode ctxt) s;
 
 val read_typ = read_typ_mode Type.mode_default;
 val read_typ_syntax = read_typ_mode Type.mode_syntax;
 val read_typ_abbrev = read_typ_mode Type.mode_abbrev;
 
 
 fun cert_typ_mode mode ctxt T =
   Type.certify_typ mode (tsig_of ctxt) T
     handle TYPE (msg, _, _) => error msg;
 
 val cert_typ = cert_typ_mode Type.mode_default;
 val cert_typ_syntax = cert_typ_mode Type.mode_syntax;
 val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev;
 
 
 
 (** prepare terms and propositions **)
 
 (* inferred types of parameters *)
 
 fun infer_type ctxt x =
   Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
 
 fun inferred_param x ctxt =
   let val p = (x, infer_type ctxt (x, dummyT))
   in (p, ctxt |> Variable.declare_term (Free p)) end;
 
 fun inferred_fixes ctxt =
   fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt;
 
 
 (* type names *)
 
 fun check_type_name {proper, strict} ctxt (c, pos) =
   if Lexicon.is_tid c then
     if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos)
     else
       let
         val reports =
           if Context_Position.is_reported ctxt pos
           then [(pos, Markup.tfree)] else [];
       in (TFree (c, default_sort ctxt (c, ~1)), reports) end
   else
     let
       val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
       val _ =
         if strict andalso not (Type.decl_logical decl)
         then error ("Bad type name: " ^ quote d ^ Position.here pos) else ();
     in (Type (d, replicate (Type.decl_args decl) dummyT), reports) end;
 
 fun read_type_name flags ctxt text =
   let
     val source = Syntax.read_input text;
     val (T, reports) = check_type_name flags ctxt (Input.source_content source);
     val _ = Context_Position.reports ctxt reports;
   in T end;
 
 
 (* constant names *)
 
 fun consts_completion_message ctxt (c, ps) =
   ps |> map (fn pos =>
     Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos))
   |> Completion.markup_report;
 
 fun check_const {proper, strict} ctxt (c, ps) =
   let
     val _ =
       Name.reject_internal (c, ps) handle ERROR msg =>
         error (msg ^ consts_completion_message ctxt (c, ps));
     fun err msg = error (msg ^ Position.here_list ps);
     val consts = consts_of ctxt;
     val fixed = if proper then NONE else Variable.lookup_fixed ctxt c;
     val (t, reports) =
       (case (fixed, Variable.lookup_const ctxt c) of
         (SOME x, NONE) =>
           let
             val reports = ps
               |> filter (Context_Position.is_reported ctxt)
               |> map (fn pos =>
                 (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free)));
           in (Free (x, infer_type ctxt (x, dummyT)), reports) end
       | (_, SOME d) =>
           let
             val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg;
             val reports = ps
               |> filter (Context_Position.is_reported ctxt)
               |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d));
           in (Const (d, T), reports) end
       | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps));
     val _ =
       (case (strict, t) of
         (true, Const (d, _)) =>
           (ignore (Consts.the_const_type consts d) handle TYPE (msg, _, _) => err msg)
       | _ => ());
   in (t, reports) end;
 
 fun read_const flags ctxt text =
   let
     val source = Syntax.read_input text;
     val (c, pos) = Input.source_content source;
     val (t, reports) = check_const flags ctxt (c, [pos]);
     val _ = Context_Position.reports ctxt reports;
   in t end;
 
 
 (* type arities *)
 
 local
 
 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
   in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end;
 
 in
 
 val read_arity =
   prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort;
 
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 
 end;
 
 
 (* read_term *)
 
 fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt);
 
 val read_term_pattern   = read_term_mode mode_pattern;
 val read_term_schematic = read_term_mode mode_schematic;
 val read_term_abbrev    = read_term_mode mode_abbrev;
 
 
 (* local abbreviations *)
 
 local
 
 fun certify_consts ctxt =
   Consts.certify {normalize = not (abbrev_mode ctxt)}
     (Context.Proof ctxt) (tsig_of ctxt) (consts_of ctxt);
 
 fun expand_binds ctxt =
   let
     val Mode {pattern, schematic, ...} = get_mode ctxt;
 
     fun reject_schematic (t as Var _) =
           error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t)
       | reject_schematic (Abs (_, _, t)) = reject_schematic t
       | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
       | reject_schematic _ = ();
   in
     if pattern then I
     else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic)
   end;
 
 in
 
 fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt;
 
 end;
 
 val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true);
 
 fun contract_abbrevs ctxt t =
   let
     val thy = theory_of ctxt;
     val consts = consts_of ctxt;
     val Mode {abbrev, ...} = get_mode ctxt;
     val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
     fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
   in
     if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
     else Pattern.rewrite_term_top thy [] [match_abbrev] t
   end;
 
 
 (* patterns *)
 
 fun prepare_patternT ctxt T =
   let
     val Mode {pattern, schematic, ...} = get_mode ctxt;
     val _ =
       pattern orelse schematic orelse
         T |> Term.exists_subtype
           (fn T as TVar (xi, _) =>
             not (Type_Infer.is_param xi) andalso
               error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T)
           | _ => false)
   in T end;
 
 
 local
 
 val dummies = Config.declare_bool ("Proof_Context.dummies", \<^here>) (K false);
 
 fun check_dummies ctxt t =
   if Config.get ctxt dummies then t
   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
 
 fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
 
 in
 
 val allow_dummies = Config.put dummies true;
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
     Type_Infer.fixate ctxt pattern #>
     pattern ? Variable.polymorphic ctxt #>
     (Same.commit o Same.map o Term.map_types_same)
       (Same.function_eq (op =) (prepare_patternT ctxt)) #>
     (if pattern then prepare_dummies else map (check_dummies ctxt))
   end;
 
 end;
 
 
 (* sort constraints *)
 
 local
 
 fun prepare_sorts_env ctxt tys =
   let
     val tsig = tsig_of ctxt;
     val defaultS = Type.defaultS tsig;
 
     val dummy_var = ("'_dummy_", ~1);
 
     fun constraint (xi, raw_S) env =
       let val (ps, S) = Term_Position.decode_positionS raw_S in
         if xi = dummy_var orelse S = dummyS then env
         else
           Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
             handle Vartab.DUP _ =>
               error ("Inconsistent sort constraints for type variable " ^
                 quote (Term.string_of_vname' xi) ^ Position.here_list ps)
       end;
 
     val env =
       Vartab.build (tys |> (fold o fold_atyps)
         (fn TFree (x, S) => constraint ((x, ~1), S)
           | TVar v => constraint v
           | _ => I));
 
     fun get_sort xi raw_S =
       if xi = dummy_var then
         Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S))
       else
         (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of
           (NONE, NONE) => defaultS
         | (NONE, SOME S) => S
         | (SOME S, NONE) => S
         | (SOME S, SOME S') =>
             if Type.eq_sort tsig (S, S') then S'
             else
               error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
                 " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
                 " for type variable " ^ quote (Term.string_of_vname' xi)));
 
     fun add_report S pos reports =
       if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then
         (pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports
       else reports;
 
     fun get_sort_reports xi raw_S =
       let
         val ps = #1 (Term_Position.decode_positionS raw_S);
         val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps);
       in fold (add_report S) ps end;
 
     val reports =
       (fold o fold_atyps)
         (fn T =>
           if Term_Position.is_positionT T then I
           else
             (case T of
               TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S
             | TVar (xi, raw_S) => get_sort_reports xi raw_S
             | _ => I)) tys [];
 
   in (map #2 reports, get_sort) end;
 
 fun replace_sortsT_same get_sort =
   Term.map_atyps_same
     (fn T =>
       if Term_Position.is_positionT T then raise Same.SAME
       else
         (case T of
           TFree (x, raw_S) => TFree (x, Same.function_eq (op =) (get_sort (x, ~1)) raw_S)
         | TVar (xi, raw_S) => TVar (xi, Same.function_eq (op =) (get_sort xi) raw_S)
         | _ => raise Same.SAME));
 
 in
 
 fun prepare_sortsT ctxt tys =
   let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys
   in (sorting_report, (Same.commit o Same.map) (replace_sortsT_same get_sort) tys) end;
 
 fun prepare_sorts ctxt tms =
   let
     val tys = rev ((fold o fold_types) cons tms []);
     val (sorting_report, get_sort) = prepare_sorts_env ctxt tys;
     val tms' = (Same.commit o Same.map o Term.map_types_same) (replace_sortsT_same get_sort) tms;
   in (sorting_report, tms') end;
 
 fun check_tfree ctxt v =
   let
     val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
     val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else ();
   in a end;
 
 end;
 
 
 (* certify terms *)
 
 local
 
 fun cert_flags flags ctxt t =
   let val t' = expand_abbrevs ctxt t in
     #1 (Sign.certify_flags flags (Context.Proof ctxt) (consts_of ctxt) (theory_of ctxt) t')
       handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg
   end;
 
 in
 
 val cert_term = cert_flags {prop = false, normalize = false};
 val cert_prop = cert_flags {prop = true, normalize = false};
 
 end;
 
 
 (* check/uncheck *)
 
 fun def_type ctxt =
   let val Mode {pattern, ...} = get_mode ctxt
   in Variable.def_type ctxt pattern end;
 
 fun standard_typ_check ctxt =
   map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt);
 
 val standard_term_check_finish = prepare_patterns;
 
 fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt);
 
 
 
 (** export results **)
 
 fun export_ goal inner outer =
   map (Assumption.export_ goal inner outer) #>
   Variable.export inner outer;
 
 val export = export_{goal = false};
 val export_goal = export_{goal = true};
 
 fun export_morphism inner outer =
   Assumption.export_morphism inner outer $>
   Variable.export_morphism inner outer;
 
 
 
 (** term bindings **)
 
 (* auto bindings *)
 
 fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
 
 
 (* match bindings *)
 
 fun simult_matches ctxt (t, pats) =
   (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of
     NONE => error "Pattern match failed!"
   | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
 
 fun maybe_bind_term (xi, t) ctxt =
   ctxt
   |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t);
 
 val bind_term = maybe_bind_term o apsnd SOME;
 
 
 (* propositions with patterns *)
 
 local
 
 fun prep_propp prep_props ctxt raw_args =
   let
     val props = prep_props ctxt (maps (map fst) raw_args);
     val props_ctxt = fold Variable.declare_term props ctxt;
     val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args;
 
     val propps = unflat raw_args (props ~~ patss);
     val binds = (maps o maps) (simult_matches props_ctxt) propps;
   in (map (map fst) propps, binds) end;
 
 in
 
 val cert_propp = prep_propp (map o cert_prop);
 val read_propp = prep_propp Syntax.read_props;
 
 end;
 
 
 
 (** theorems **)
 
 (* fact_tac *)
 
 local
 
 fun comp_hhf_tac ctxt th i st =
   PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
     (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st;
 
 fun comp_incr_tac _ [] _ = no_tac
   | comp_incr_tac ctxt (th :: ths) i =
       (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND
       comp_incr_tac ctxt ths i;
 
 val vacuous_facts = [Drule.termI];
 
 in
 
 fun potential_facts ctxt prop =
   let
     val body = Term.strip_all_body prop;
     val vacuous =
       filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts
       |> map (rpair Position.none);
   in Facts.could_unify (facts_of ctxt) body @ vacuous end;
 
 fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
 
 fun some_fact_tac ctxt =
   SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i);
 
 end;
 
 
 (* lookup facts *)
 
 fun lookup_fact ctxt name =
   let
     val context = Context.Proof ctxt;
     val thy = Proof_Context.theory_of ctxt;
   in
     (case Facts.lookup context (facts_of ctxt) name of
       NONE => Facts.lookup context (Global_Theory.facts_of thy) name
     | some => some)
   end;
 
 
 (* retrieve facts *)
 
 val dynamic_facts_dummy = Config.declare_bool ("dynamic_facts_dummy_", \<^here>) (K false);
 
 local
 
 fun retrieve_global context =
   Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context));
 
 fun retrieve_generic (context as Context.Proof ctxt) arg =
       (Facts.retrieve context (facts_of ctxt) arg handle ERROR local_msg =>
         (retrieve_global context arg handle ERROR _ => error local_msg))
   | retrieve_generic context arg = retrieve_global context arg;
 
 fun retrieve pick context (Facts.Fact s) =
       let
         val ctxt = Context.the_proof context;
         val pos = Syntax.read_input_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);
         fun err ps msg =
           error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop);
 
         val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
         fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
         val results = map_filter (try (apfst prove)) (potential_facts ctxt prop');
         val (thm, thm_pos) =
           (case distinct (eq_fst Thm.eq_thm_prop) results of
             [res] => res
           | [] => err [] "Failed to retrieve literal fact"
           | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
 
         val markup = Position.entity_markup Markup.literal_factN ("", thm_pos);
         val _ = Context_Position.report_generic context pos markup;
       in pick true ("", thm_pos) [thm] end
   | retrieve pick context (Facts.Named ((xname, pos), sel)) =
       let
         val thy = Context.theory_of context;
         fun immediate thms = {name = xname, dynamic = false, thms = map (Thm.transfer thy) thms};
         val {name, dynamic, thms} =
           (case xname of
             "" => immediate [Drule.dummy_thm]
           | "_" => immediate [Drule.asm_rl]
           | "nothing" => immediate []
           | _ => retrieve_generic context (xname, pos));
         val thms' =
           if dynamic andalso Config.get_generic context dynamic_facts_dummy
           then [Drule.free_dummy_thm]
           else Facts.select (Facts.Named ((name, pos), sel)) thms;
       in pick (dynamic andalso is_none sel) (name, pos) thms' end;
 
 in
 
 val get_fact_generic =
   retrieve (fn dynamic => fn (name, _) => fn thms =>
     (if dynamic then SOME name else NONE, thms));
 
 val get_fact = retrieve (K (K I)) o Context.Proof;
 val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
 
 fun get_thms ctxt = get_fact ctxt o Facts.named;
 fun get_thm ctxt = get_fact_single ctxt o Facts.named;
 
 end;
 
 
 (* inner statement mode *)
 
 val inner_stmt = Config.declare_bool ("inner_stmt", \<^here>) (K false);
 fun is_stmt ctxt = Config.get ctxt inner_stmt;
 val set_stmt = Config.put inner_stmt;
 val restore_stmt = set_stmt o is_stmt;
 
 
 (* facts *)
 
 fun add_thms_dynamic arg ctxt =
   ctxt |> map_facts_result (Facts.add_dynamic (Context.Proof ctxt) arg);
 
 local
 
 fun add_facts {index} arg ctxt = ctxt
   |> map_facts_result (Facts.add_static (Context.Proof ctxt) {strict = false, index = index} arg);
 
 fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2
   | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b));
 
 fun full_name_pos ctxt b = (full_name ctxt b, Binding.default_pos_of b);
 
 in
 
 fun add_thms_lazy kind (b, ths) ctxt =
   let
     val name_pos = full_name_pos ctxt b;
     val ths' =
       Global_Theory.check_thms_lazy ths
       |> Lazy.map_finished
           (Global_Theory.name_thms Global_Theory.unofficial1 name_pos #> map (Thm.kind_rule kind));
     val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
   in ctxt' end;
 
 fun note_thms kind ((b, more_atts), facts) ctxt =
   let
     val name_pos = full_name_pos ctxt b;
     fun app_fact (thms, atts) =
       fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) thms;
     val (thms', ctxt') =
       fold_maps app_fact (Global_Theory.name_facts Global_Theory.unofficial1 name_pos facts) ctxt;
     val thms'' = Global_Theory.name_thms Global_Theory.unofficial2 name_pos thms';
     val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms'');
   in ((#1 name_pos, thms''), ctxt'') end;
 
 val note_thmss = fold_map o note_thms;
 
 fun put_thms index thms ctxt = ctxt
   |> map_naming (K Name_Space.local_naming)
   |> Context_Position.set_visible false
   |> update_facts {index = index} (apfst Binding.name thms)
   |> Context_Position.restore_visible ctxt
   |> restore_naming ctxt;
 
 end;
 
 fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
 
 
 
 (** basic logical entities **)
 
 (* variables *)
 
 fun declare_var (x, opt_T, mx) ctxt =
   let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx)
   in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
 
 fun add_syntax vars ctxt =
   map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt;
 
 fun check_var internal b =
   let
     val x = Variable.check_name b;
     val check = if internal then Name.reject_skolem else Name.reject_internal;
     val _ =
       if can check (x, []) andalso Symbol_Pos.is_identifier x then ()
       else error ("Bad name: " ^ Binding.print b);
   in x end;
 
 local
 
 fun check_mixfix ctxt (b, T, mx) =
   let
     val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt;
     val mx' = Mixfix.reset_pos mx;
     val _ = add_syntax [(x, T, if Context_Position.reports_enabled ctxt then mx else mx')] ctxt';
   in mx' end;
 
 fun prep_var prep_typ internal (b, raw_T, mx) ctxt =
   let
     val x = check_var internal b;
     fun cond_tvars T =
       if internal then T
       else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
     val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T;
     val (T, ctxt') = ctxt |> declare_var (x, opt_T, mx);
     val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt' (b, T, mx);
   in ((b, SOME T, mx'), ctxt') end;
 
 in
 
 val read_var = prep_var Syntax.read_typ false;
 val cert_var = prep_var cert_typ true;
 
 end;
 
 
 (* syntax *)
 
 fun check_syntax_const ctxt (c, pos) =
-  if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
+  if is_some (Syntax.lookup_const (syntax_of ctxt) c) then c
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
 fun syntax add mode args ctxt =
   let val args' = map (pair Local_Syntax.Const) args
   in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end;
 
 fun generic_syntax add mode args =
   Context.mapping (Sign.syntax add mode args) (syntax add mode args);
 
 
 (* notation *)
 
 local
 
 fun type_syntax (Type (c, args), mx) =
       SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx))
   | type_syntax _ = NONE;
 
 fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
   | const_syntax ctxt (Const (c, _), mx) =
       (case try (Consts.type_scheme (consts_of ctxt)) c of
         SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx))
       | NONE => NONE)
   | const_syntax _ _ = NONE;
 
 fun gen_notation make_syntax add mode args ctxt =
   ctxt |> map_syntax_idents
     (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args));
 
 in
 
 val type_notation = gen_notation (K type_syntax);
 val notation = gen_notation const_syntax;
 
 fun generic_type_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (T, mx) =>
       let
         val T' = Morphism.typ phi T;
         val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false);
       in if similar then SOME (T', mx) else NONE end);
   in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
 
 fun generic_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (t, mx) =>
       let val t' = Morphism.term phi t
       in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
   in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
 
 end;
 
 
 (* aliases *)
 
 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
 
 
 (* local constants *)
 
 fun add_const_constraint (c, opt_T) ctxt =
   let
     fun prepT raw_T =
       let val T = cert_typ ctxt raw_T
       in cert_term ctxt (Const (c, T)); T end;
   in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end;
 
 fun add_abbrev mode (b, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
       |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
   in
     ctxt
     |> (map_consts o apfst) (K consts')
     |> Variable.declare_term rhs
     |> pair (lhs, rhs)
   end;
 
 fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
 
 fun generic_add_abbrev mode arg =
   Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg);
 
 fun generic_revert_abbrev mode arg =
   Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg);
 
 
 (* fixes *)
 
 local
 
 fun gen_fixes prep_var raw_vars ctxt =
   let
     val (vars, _) = fold_map prep_var raw_vars ctxt;
     val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt;
     val _ =
       Context_Position.reports ctxt'
         (flat (map2 (fn x => fn pos =>
           [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)])
             xs (map (Binding.pos_of o #1) vars)));
     val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars;
     val (Ts, ctxt'') = fold_map declare_var vars' ctxt';
     val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars';
   in (xs, add_syntax vars'' ctxt'') end;
 
 in
 
 val add_fixes = gen_fixes cert_var;
 val add_fixes_cmd = gen_fixes read_var;
 
 end;
 
 
 
 (** assumptions **)
 
 local
 
 fun gen_assms prep_propp exp args ctxt =
   let
     val (propss, binds) = prep_propp ctxt (map snd args);
     val props = flat propss;
   in
     ctxt
     |> fold Variable.declare_term props
     |> tap (Variable.warn_extra_tfrees ctxt)
     |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
     |-> (fn premss =>
       auto_bind_facts props
       #> fold Variable.bind_term binds
       #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
   end;
 
 in
 
 val add_assms = gen_assms cert_propp;
 val add_assms_cmd = gen_assms read_propp;
 
 end;
 
 
 
 (** cases **)
 
 fun dest_cases prev_ctxt ctxt =
   let
     val serial_of = #serial oo (Name_Space.the_entry o Name_Space.space_of_table);
     val ignored =
       (case prev_ctxt of
         NONE => Intset.empty
       | SOME ctxt0 =>
           let val cases0 = cases_of ctxt0 in
             Intset.build (cases0 |> Name_Space.fold_table (fn (a, _) =>
               Intset.insert (serial_of cases0 a)))
           end);
      val cases = cases_of ctxt;
   in
     Name_Space.fold_table (fn (a, c) =>
       let val i = serial_of cases a
       in not (Intset.member ignored i) ? cons (i, (a, c)) end) cases []
     |> sort (int_ord o apply2 #1) |> map #2
   end;
 
 local
 
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
 fun update_case _ ("", _) cases = cases
   | update_case _ (name, NONE) cases = Name_Space.del_table name cases
   | update_case context (name, SOME c) cases =
       #2 (Name_Space.define context false (Binding.name name, c) cases);
 
 fun fix (b, T) ctxt =
   let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
   in (Free (x, T), ctxt') end;
 
 in
 
 fun update_cases args ctxt =
   let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
   in map_cases (fold (update_case context) args) ctxt end;
 
 fun case_result c ctxt =
   let
     val Rule_Cases.Case {fixes, ...} = c;
     val (ts, ctxt') = ctxt |> fold_map fix fixes;
     val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
     |> fold (maybe_bind_term o drop_schematic) binds
     |> update_cases (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;
 
 val apply_case = apfst fst oo case_result;
 
 fun check_case ctxt internal (name, pos) param_specs =
   let
     val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
 
     val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
       | replace [] ys = ys
       | replace (_ :: _) [] =
           error ("Too many parameters for case " ^ quote name ^ Position.here pos);
     val fixes' = replace param_specs fixes;
     val binds' = map drop_schematic binds;
   in
     if null (fold (Term.add_tvarsT o snd) fixes []) andalso
       null (fold (fold Term.add_vars o snd) assumes []) then
         Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
     else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos)
   end;
 
 end;
 
 
 (* structured statements *)
 
 type stmt =
  {vars: ((binding * typ option * mixfix) * (string * term)) list,
   propss: term list list,
   binds: (indexname * term) list,
   result_binds: (indexname * term) list};
 
 type statement =
  {fixes: (string * term) list,
   assumes: term list list,
   shows: term list list,
   result_binds: (indexname * term option) list,
   text: term,
   result_text: term};
 
 local
 
 fun export_binds ctxt' ctxt params binds =
   let
     val rhss =
       map (the_list o Option.map (Logic.close_term params) o snd) binds
       |> burrow (Variable.export_terms ctxt' ctxt)
       |> map (try the_single);
   in map fst binds ~~ rhss end;
 
 fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt =
   let
     val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
     val xs = map (Variable.check_name o #1) vars;
     val (xs', fixes_ctxt) = add_fixes vars vars_ctxt;
 
     val (propss, binds) = prep_propp fixes_ctxt raw_propps;
     val (ps, params_ctxt) = fixes_ctxt
       |> (fold o fold) Variable.declare_term propss
       |> fold_map inferred_param xs';
     val params = xs ~~ map Free ps;
 
     val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
     val binds' = binds
       |> map (apsnd SOME)
       |> export_binds params_ctxt ctxt params
       |> map (apsnd the);
 
     val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
     val result : stmt =
       {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'};
   in (result, params_ctxt) end;
 
 fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
   let
     val ((fixes, (assumes, shows), binds), ctxt') = ctxt
       |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
       |-> (fn {vars, propss, binds, ...} =>
         fold Variable.bind_term binds #>
         pair (map #2 vars, chop (length raw_assumes) propss, binds));
     val binds' =
       (Auto_Bind.facts ctxt' (flat shows) @
         (case try List.last (flat shows) of
           NONE => []
         | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
       |> export_binds ctxt' ctxt fixes;
 
     val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows));
     val text' = singleton (Variable.export_terms ctxt' ctxt) text;
 
     val result : statement =
      {fixes = fixes,
       assumes = assumes,
       shows = shows,
       result_binds = binds',
       text = text,
       result_text = text'};
   in (result, ctxt') end;
 
 in
 
 val cert_stmt = prep_stmt cert_var cert_propp;
 val read_stmt = prep_stmt read_var read_propp;
 val cert_statement = prep_statement cert_var cert_propp;
 val read_statement = prep_statement read_var read_propp;
 
 end;
 
 
 
 (** print context information **)
 
 (* local syntax *)
 
-val print_syntax = Syntax.print_syntax o syn_of;
+val print_syntax = Syntax.print_syntax o syntax_of;
 
 
 (* abbreviations *)
 
 fun pretty_abbrevs verbose show_globals ctxt =
   let
     val space = const_space ctxt;
     val (constants, global_constants) =
       apply2 (#constants o Consts.dest) (#consts (rep_data ctxt));
     val globals = Symtab.make global_constants;
     fun add_abbr (_, (_, NONE)) = I
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
     val abbrevs = Name_Space.markup_entries verbose ctxt space (fold add_abbr constants []);
   in
     if null abbrevs then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
   end;
 
 fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true;
 
 
 (* term bindings *)
 
 fun pretty_term_bindings ctxt =
   let
     val binds = Variable.binds_of ctxt;
     fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t));
   in
     if Vartab.is_empty binds then []
     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
   end;
 
 
 (* local facts *)
 
 fun pretty_local_facts verbose ctxt =
   let
     val facts = facts_of ctxt;
     val props = map #1 (Facts.props facts);
     val local_facts =
       (if null props then [] else [("<unnamed>", props)]) @
       Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
   in
     if null local_facts then []
     else
       [Pretty.big_list "local facts:"
         (map #1 (sort_by (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))]
   end;
 
 fun print_local_facts verbose ctxt =
   Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
 
 
 (* named local contexts *)
 
 local
 
 fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) =
   let
     val prt_name = pretty_name ctxt;
     val prt_term = Syntax.pretty_term ctxt;
 
     fun prt_let (xi, t) = Pretty.block
       [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1,
         Pretty.quote (prt_term t)];
 
     fun prt_asm (a, ts) =
       Pretty.block (Pretty.breaks
         ((if a = "" then [] else [prt_name a, Pretty.str ":"]) @
           map (Pretty.quote o prt_term) ts));
 
     fun prt_sect _ _ _ [] = []
       | prt_sect head sep prt xs =
           [Pretty.block (Pretty.breaks (head ::
             flat (separate sep (map (single o prt) xs))))];
   in
     Pretty.block
       (prt_name name :: Pretty.str ":" :: Pretty.fbrk ::
         Pretty.fbreaks
           (prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @
            prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
              (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
            (if forall (null o #2) asms then []
             else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
            prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs))
   end;
 
 in
 
 fun pretty_cases ctxt =
   let
     val cases =
       dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) =>
         (name, (fixes, case_result c ctxt)));
   in
     if null cases then []
     else [Pretty.big_list "cases:" (map pretty_case cases)]
   end;
 
 end;
 
 fun print_cases_proof ctxt0 ctxt =
   let
     fun trim_name x = if Name.is_internal x then Name.clean x else "_";
     val trim_names = map trim_name #> drop_suffix (equal "_");
 
     fun print_case name xs =
       (case trim_names xs of
         [] => print_name ctxt name
       | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs'))));
 
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
 
     fun indentation depth = prefix (Symbol.spaces (2 * depth));
 
     fun print_proof depth (name, Rule_Cases.Case {fixes, binds, cases, ...}) =
           let
             val indent = indentation depth;
             val head = indent ("case " ^ print_case name (map (Binding.name_of o #1) fixes));
             val tail =
               if null cases then
                 let val concl =
                   if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
                   then Rule_Cases.case_conclN else Auto_Bind.thesisN
                 in indent ("then show ?" ^ concl ^ " sorry") end
               else print_proofs depth cases;
           in head ^ "\n" ^ tail end
     and print_proofs 0 [] = ""
       | print_proofs depth cases =
           let
             val indent = indentation depth;
             val body = map (print_proof (depth + 1)) cases |> separate (indent "next")
           in
             if depth = 0 then body @ [indent "qed"]
             else if length cases = 1 then body
             else indent "{" :: body @ [indent "}"]
           end |> cat_lines;
   in
     (case print_proofs 0 (dest_cases (SOME ctxt0) ctxt) of
       "" => ""
     | s => "Proof outline with cases:\n" ^ Active.sendback_markup_command s)
   end;
 
 
 (* core context *)
 
 val debug = Config.declare_bool ("Proof_Context.debug", \<^here>) (K false);
 val verbose = Config.declare_bool ("Proof_Context.verbose", \<^here>) (K false);
 
 fun pretty_ctxt ctxt =
   if not (Config.get ctxt debug) then []
   else
     let
       val prt_term = Syntax.pretty_term ctxt;
 
       (*structures*)
       val {structs, ...} = Syntax_Trans.get_idents ctxt;
       val prt_structs =
         if null structs then []
         else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
           Pretty.commas (map Pretty.str structs))];
 
       (*fixes*)
       fun prt_fix (x, x') =
         if x = x' then Pretty.str x
         else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')];
       val fixes =
         filter_out ((Name.is_internal orf member (op =) structs) o #1)
           (Variable.dest_fixes ctxt);
       val prt_fixes =
         if null fixes then []
         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
           Pretty.commas (map prt_fix fixes))];
 
       (*assumptions*)
       val prt_assms =
         (case Assumption.all_prems_of ctxt of
           [] => []
         | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]);
     in prt_structs @ prt_fixes @ prt_assms end;
 
 
 (* main context *)
 
 fun pretty_context ctxt =
   let
     val verbose = Config.get ctxt verbose;
     fun verb f x = if verbose then f (x ()) else [];
 
     val prt_term = Syntax.pretty_term ctxt;
     val prt_typ = Syntax.pretty_typ ctxt;
     val prt_sort = Syntax.pretty_sort ctxt;
 
     (*theory*)
     val pretty_thy = Pretty.block
       [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)];
 
     (*defaults*)
     fun prt_atom prt prtT (x, X) = Pretty.block
       [prt x, Pretty.str " ::", Pretty.brk 1, prtT X];
 
     fun prt_var (x, ~1) = prt_term (Syntax.free x)
       | prt_var xi = prt_term (Syntax.var xi);
 
     fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
       | prt_varT xi = prt_typ (TVar (xi, []));
 
     val prt_defT = prt_atom prt_var prt_typ;
     val prt_defS = prt_atom prt_varT prt_sort;
 
     val (types, sorts) = Variable.constraints_of ctxt;
   in
     verb single (K pretty_thy) @
     pretty_ctxt ctxt @
     verb (pretty_abbrevs true false) (K ctxt) @
     verb pretty_term_bindings (K ctxt) @
     verb (pretty_local_facts true) (K ctxt) @
     verb pretty_cases (K ctxt) @
     verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @
     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
   end;
 
 end;
 
 val show_abbrevs = Proof_Context.show_abbrevs;
diff --git a/src/Pure/Syntax/local_syntax.ML b/src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML
+++ b/src/Pure/Syntax/local_syntax.ML
@@ -1,125 +1,125 @@
 (*  Title:      Pure/Syntax/local_syntax.ML
     Author:     Makarius
 
 Local syntax depending on theory syntax, with special support for
 implicit structure references.
 *)
 
 signature LOCAL_SYNTAX =
 sig
   type T
-  val syn_of: T -> Syntax.syntax
+  val syntax_of: T -> Syntax.syntax
   val init: theory -> T
   val rebuild: theory -> T -> T
   datatype kind = Type | Const | Fixed
   val add_syntax: Proof.context -> (kind * (string * typ * mixfix)) list ->
     T -> {structs: string list, fixes: string list} option * T
   val set_mode: Syntax.mode -> T -> T
   val restore_mode: T -> T -> T
   val update_modesyntax: Proof.context -> bool -> Syntax.mode ->
     (kind * (string * typ * mixfix)) list ->
     T -> {structs: string list, fixes: string list} option * T
 end;
 
 structure Local_Syntax: LOCAL_SYNTAX =
 struct
 
 (* datatype T *)
 
 type local_mixfix =
   (string * bool) *  (*name, fixed?*)
   ((bool * bool * Syntax.mode) * (string * typ * mixfix));  (*type?, add?, mode, declaration*)
 
 datatype T = Syntax of
  {thy_syntax: Syntax.syntax,
   local_syntax: Syntax.syntax,
   mode: Syntax.mode,
   mixfixes: local_mixfix list};
 
 fun make_syntax (thy_syntax, local_syntax, mode, mixfixes) =
   Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, mode = mode, mixfixes = mixfixes};
 
 fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes}) =
   make_syntax (f (thy_syntax, local_syntax, mode, mixfixes));
 
 fun is_consistent thy (Syntax {thy_syntax, ...}) =
-  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
+  Syntax.eq_syntax (Sign.syntax_of thy, thy_syntax);
 
-fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
+fun syntax_of (Syntax {local_syntax, ...}) = local_syntax;
 
 
 (* build syntax *)
 
 fun build_syntax thy mode mixfixes =
   let
-    val thy_syntax = Sign.syn_of thy;
+    val thy_syntax = Sign.syntax_of thy;
     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
       | update_gram ((false, add, m), decls) =
           Syntax.update_const_gram add (Sign.logical_types thy) m decls;
 
     val local_syntax = thy_syntax
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
   in make_syntax (thy_syntax, local_syntax, mode, mixfixes) end;
 
 fun init thy =
-  let val thy_syntax = Sign.syn_of thy
+  let val thy_syntax = Sign.syntax_of thy
   in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, []) end;
 
 fun rebuild thy (syntax as Syntax {mode, mixfixes, ...}) =
   if is_consistent thy syntax then syntax
   else build_syntax thy mode mixfixes;
 
 
 (* mixfix declarations *)
 
 datatype kind = Type | Const | Fixed;
 
 local
 
 fun prep_mixfix _ _ (_, (_, _, Structure _)) = NONE
   | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
   | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
   | prep_mixfix add mode (Fixed, (x, T, mx)) =
       SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
 
 fun prep_struct (Fixed, (c, _, Structure _)) = SOME c
   | prep_struct (_, (c, _, Structure _)) = error ("Bad structure mixfix declaration for " ^ quote c)
   | prep_struct _ = NONE;
 
 in
 
 fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) =
   (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of
     [] => (NONE, syntax)
   | decls =>
       let
         val new_mixfixes = map_filter (prep_mixfix add mode) decls;
         val new_structs = map_filter prep_struct decls;
         val mixfixes' = rev new_mixfixes @ mixfixes;
 
         val idents = Syntax_Trans.get_idents ctxt;
         val idents' =
           {structs =
             if add then #structs idents @ new_structs
             else subtract (op =) new_structs (#structs idents),
            fixes = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []};
 
         val syntax' = build_syntax (Proof_Context.theory_of ctxt) mode mixfixes';
       in (if idents = idents' then NONE else SOME idents', syntax') end);
 
 fun add_syntax ctxt = update_syntax ctxt true;
 
 end;
 
 
 (* syntax mode *)
 
 fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes) =>
   (thy_syntax, local_syntax, mode, mixfixes));
 
 fun restore_mode (Syntax {mode, ...}) = set_mode mode;
 
 fun update_modesyntax ctxt add mode args syntax =
   syntax |> set_mode mode |> update_syntax ctxt add args ||> restore_mode syntax;
 
 end;
diff --git a/src/Pure/Syntax/syntax_phases.ML b/src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML
+++ b/src/Pure/Syntax/syntax_phases.ML
@@ -1,1017 +1,1017 @@
 (*  Title:      Pure/Syntax/syntax_phases.ML
     Author:     Makarius
 
 Main phases of inner syntax processing, with standard implementations
 of parse/unparse operations.
 *)
 
 signature SYNTAX_PHASES =
 sig
   val markup_free: Proof.context -> string -> Markup.T list
   val reports_of_scope: Position.T list -> Position.report list
   val decode_sort: term -> sort
   val decode_typ: term -> typ
   val decode_term: Proof.context ->
     Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
   val print_checks: Proof.context -> unit
   val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
     Context.generic -> Context.generic
   val term_check: int -> string -> (Proof.context -> term list -> term list) ->
     Context.generic -> Context.generic
   val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
     Context.generic -> Context.generic
   val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
     Context.generic -> Context.generic
   val typ_check': int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
   val term_check': int -> string ->
     (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
   val typ_uncheck': int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
     Context.generic -> Context.generic
   val term_uncheck': int -> string ->
     (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
 end
 
 structure Syntax_Phases: SYNTAX_PHASES =
 struct
 
 (** markup logical entities **)
 
 fun markup_class ctxt c =
   [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
 
 fun markup_type ctxt c =
   [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
 
 fun markup_const ctxt c =
   [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
 
 fun markup_free ctxt x =
   Variable.markup ctxt x ::
   (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    then [Variable.markup_fixed ctxt x]
    else []);
 
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 
 fun markup_bound def ps (name, id) =
   Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity ctxt c =
-  (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
+  (case Syntax.lookup_const (Proof_Context.syntax_of ctxt) c of
     SOME "" => []
   | SOME b => markup_entity ctxt b
   | NONE => c |> Lexicon.unmark
      {case_class = markup_class ctxt,
       case_type = markup_type ctxt,
       case_const = markup_const ctxt,
       case_fixed = markup_free ctxt,
       case_default = K []});
 
 
 
 (** reports of implicit variable scope **)
 
 fun reports_of_scope [] = []
   | reports_of_scope (def_pos :: ps) =
       let
         val id = serial ();
         fun entity def = Position.make_entity_markup def id "" ("", def_pos);
       in
         map (rpair Markup.bound) (def_pos :: ps) @
         ((def_pos, entity {def = true}) :: map (rpair (entity {def = false})) ps)
       end;
 
 
 
 (** decode parse trees **)
 
 (* decode_sort *)
 
 fun decode_sort tm =
   let
     fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
 
     fun class s = Lexicon.unmark_class s handle Fail _ => err ();
 
     fun classes (Const (s, _)) = [class s]
       | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
       | classes _ = err ();
 
     fun sort (Const ("_dummy_sort", _)) = dummyS
       | sort (Const ("_topsort", _)) = []
       | sort (Const ("_sort", _) $ cs) = classes cs
       | sort (Const (s, _)) = [class s]
       | sort _ = err ();
   in sort tm end;
 
 
 (* decode_typ *)
 
 fun decode_pos (Free (s, _)) =
       if is_some (Term_Position.decode s) then SOME s else NONE
   | decode_pos _ = NONE;
 
 fun decode_typ tm =
   let
     fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
 
     fun typ ps sort tm =
       (case tm of
         Const ("_tfree", _) $ t => typ ps sort t
       | Const ("_tvar", _) $ t => typ ps sort t
       | Const ("_ofsort", _) $ t $ s =>
           (case decode_pos s of
             SOME p => typ (p :: ps) sort t
           | NONE =>
               if is_none sort then typ ps (SOME (decode_sort s)) t
               else err ())
       | Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s)
       | Free (x, _) => TFree (x, ps @ the_default dummyS sort)
       | Var (xi, _) => TVar (xi, ps @ the_default dummyS sort)
       | _ =>
           if null ps andalso is_none sort then
             let
               val (head, args) = Term.strip_comb tm;
               val a =
                 (case head of
                   Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
                 | _ => err ());
             in Type (a, map (typ [] NONE) args) end
           else err ());
   in typ [] NONE tm end;
 
 
 (* parsetree_to_ast *)
 
 fun parsetree_to_ast ctxt trf parsetree =
   let
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report pos = Position.store_reports reports [pos];
     val append_reports = Position.append_reports reports;
 
     fun report_pos tok =
       if Lexicon.suppress_markup tok then Position.none
       else Lexicon.pos_of_token tok;
 
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
       | SOME f => f ctxt args);
 
     fun asts_of_token tok =
       if Lexicon.valued_token tok
       then [Ast.Variable (Lexicon.str_of_token tok)]
       else [];
 
     fun ast_of_position tok =
       Ast.Variable (Term_Position.encode (report_pos tok));
 
     fun ast_of_dummy a tok =
       Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
 
     fun asts_of_position c tok =
       [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
 
     and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
           let
             val pos = report_pos tok;
             val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_class c)] end
       | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
           let
             val pos = report_pos tok;
             val (Type (c, _), rs) =
               Proof_Context.check_type_name {proper = true, strict = false} ctxt
                 (Lexicon.str_of_token tok, pos);
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
       | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
       | asts_of (Parser.Node (a as "\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
           [ast_of_dummy a tok]
       | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
           [ast_of_dummy a tok]
       | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
           [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
       | asts_of (Parser.Node (a, pts)) =
           let
             val _ = pts |> List.app
               (fn Parser.Node _ => () | Parser.Tip tok =>
                 if Lexicon.valued_token tok then ()
                 else report (report_pos tok) (markup_entity ctxt) a);
           in [trans a (maps asts_of pts)] end
       | asts_of (Parser.Tip tok) = asts_of_token tok
 
     and ast_of pt =
       (case asts_of pt of
         [ast] => ast
       | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
 
     val ast = Exn.result ast_of parsetree;
   in (! reports, ast) end;
 
 
 (* ast_to_term *)
 
 fun ast_to_term ctxt trf =
   let
     fun trans a args =
       (case trf a of
         NONE => Term.list_comb (Syntax.const a, args)
       | SOME f => f ctxt args);
 
     fun term_of (Ast.Constant a) = trans a []
       | term_of (Ast.Variable x) = Lexicon.read_var x
       | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
           trans a (map term_of asts)
       | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
           Term.list_comb (term_of ast, map term_of asts)
       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
   in term_of end;
 
 
 (* decode_term -- transform parse tree into raw term *)
 
 fun decode_const ctxt (c, ps) =
   let
     val (Const (c', _), reports) =
       Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps);
   in (c', reports) end;
 
 local
 
 fun get_free ctxt x =
   let
     val fixed = Variable.lookup_fixed ctxt x;
     val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
     val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
   in
     if Variable.is_const ctxt x then NONE
     else if is_some fixed then fixed
     else if not is_const orelse is_declared then SOME x
     else NONE
   end;
 
 in
 
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
         val reports = Unsynchronized.ref reports0;
         fun report ps = Position.store_reports reports ps;
         val append_reports = Position.append_reports reports;
 
         fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
               | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
           | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
               (case Term_Position.decode_position typ of
                 SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
               | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
           | decode _ qs bs (Abs (x, T, t)) =
               let
                 val id = serial ();
                 val _ = report qs (markup_bound {def = true} qs) (x, id);
               in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
           | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
           | decode ps _ _ (Const (a, T)) =
               (case try Lexicon.unmark_fixed a of
                 SOME x => (report ps (markup_free ctxt) x; Free (x, T))
               | NONE =>
                   let
                     val c =
                       (case try Lexicon.unmark_const a of
                         SOME c => c
                       | NONE => #1 (decode_const ctxt (a, [])));
                     val _ = report ps (markup_const ctxt) c;
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, T)) =
               ((Name.reject_internal (a, ps) handle ERROR msg =>
                   error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
                 (case get_free ctxt a of
                   SOME x => (report ps (markup_free ctxt) x; Free (x, T))
                 | NONE =>
                     let
                       val (c, rs) = decode_const ctxt (a, ps);
                       val _ = append_reports rs;
                     in Const (c, T) end))
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
                 SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t)
               | NONE => t);
 
         val tm' = Exn.result (fn () => decode [] [] [] tm) ();
       in (! reports, tm') end;
 
 end;
 
 
 
 (** parse **)
 
 (* results *)
 
 fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
 
 fun report_result ctxt pos ambig_msgs results =
   (case (proper_results results, failed_results results) of
     ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; Exn.reraise exn)
   | ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x)
   | _ =>
       if null ambig_msgs then
         error ("Parse error: ambiguous syntax" ^ Position.here pos)
       else error (cat_lines ambig_msgs));
 
 
 (* parse raw asts *)
 
 fun parse_asts ctxt raw root (syms, pos) =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
     val _ = Context_Position.reports ctxt (maps Lexicon.reports_of_token toks);
 
     val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
         error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks)));
     val len = length pts;
 
     val limit = Config.get ctxt Syntax.ambiguity_limit;
     val ambig_msgs =
       if len <= 1 then []
       else
         [cat_lines
           (("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^
             " produces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
             map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
               (take limit pts))];
 
   in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
 
 fun parse_tree ctxt root input =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val tr = Syntax.parse_translation syn;
     val parse_rules = Syntax.parse_rules syn;
     val (ambig_msgs, asts) = parse_asts ctxt false root input;
     val results =
       (map o apsnd o Exn.maps_res)
         (Ast.normalize ctxt parse_rules #> Exn.result (ast_to_term ctxt tr)) asts;
   in (ambig_msgs, results) end;
 
 
 (* parse logical entities *)
 
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
     Markup.markup_report (Context_Position.reported_text ctxt pos (Markup.bad ()) ""));
 
 fun parse_sort ctxt =
   Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
     (fn (syms, pos) =>
       parse_tree ctxt "sort" (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode_sort
       |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
       handle ERROR msg => parse_failed ctxt pos msg "sort");
 
 fun parse_typ ctxt =
   Syntax.parse_input ctxt Term_XML.Decode.typ Markup.language_type
     (fn (syms, pos) =>
       parse_tree ctxt "type" (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode_typ
       handle ERROR msg => parse_failed ctxt pos msg "type");
 
 fun parse_term is_prop ctxt =
   let
     val (markup, kind, root, constrain) =
       if is_prop
       then (Markup.language_prop, "prop", "prop", Type.constraint propT)
       else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
     val decode = constrain o Term_XML.Decode.term (Proof_Context.consts_of ctxt);
   in
     Syntax.parse_input ctxt decode markup
       (fn (syms, pos) =>
         let
           val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
           val parsed_len = length (proper_results results);
 
           val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning;
           val limit = Config.get ctxt Syntax.ambiguity_limit;
 
           (*brute-force disambiguation via type-inference*)
           fun check t =
             (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t)
               handle exn as ERROR _ => Exn.Exn exn;
 
           fun par_map xs = Par_List.map' {name = "Syntax_Phases.parse_term", sequential = false} xs;
           val results' =
             if parsed_len > 1 then (grouped 10 par_map o apsnd o Exn.maps_res) check results
             else results;
           val reports' = fst (hd results');
 
           val errs = map snd (failed_results results');
           val checked = map snd (proper_results results');
           val checked_len = length checked;
 
           val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt);
         in
           if checked_len = 0 then
             report_result ctxt pos []
               [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
           else if checked_len = 1 then
             (if not (null ambig_msgs) andalso ambiguity_warning andalso
                 Context_Position.is_visible ctxt then
               warning
                 (cat_lines (ambig_msgs @
                   ["Fortunately, only one parse tree is well-formed and type-correct,\n\
                    \but you may still want to disambiguate your grammar or your input."]))
              else (); report_result ctxt pos [] results')
           else
             report_result ctxt pos []
               [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @
                 (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
                   (if checked_len <= limit then ""
                    else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
                   map (Pretty.string_of o Pretty.item o single o pretty_term)
                     (take limit checked))))))]
         end handle ERROR msg => parse_failed ctxt pos msg kind)
   end;
 
 
 (* parse_ast_pattern *)
 
 fun parse_ast_pattern ctxt (root, str) =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
 
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report ps = Position.store_reports reports ps;
 
     fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c);
     fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x);
     fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
     and decode ps (Ast.Constant c) = decode_const ps c
       | decode ps (Ast.Variable x) =
           if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
           then decode_const ps x
           else decode_var ps x
       | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
           if member (op =) Term_Position.markers c then
             (case Term_Position.decode x of
               SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
             | NONE => decode_appl ps asts)
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
     val source = Syntax.read_input str;
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
     val ast =
       parse_asts ctxt true root (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode [];
     val _ = Context_Position.reports_text ctxt (! reports);
   in ast end;
 
 
 
 (** encode parse trees **)
 
 (* term_of_sort *)
 
 fun term_of_sort S =
   let
     val class = Syntax.const o Lexicon.mark_class;
 
     fun classes [c] = class c
       | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
   in
     if S = dummyS then Syntax.const "_dummy_sort"
     else
       (case S of
         [] => Syntax.const "_topsort"
       | [c] => class c
       | cs => Syntax.const "_sort" $ classes cs)
   end;
 
 
 (* term_of_typ *)
 
 fun term_of_typ ctxt ty =
   let
     val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
 
     fun ofsort t raw_S =
       if show_sorts then
         let val S = #2 (Term_Position.decode_positionS raw_S)
         in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
       else t;
 
     fun term_of (Type (a, Ts)) =
           Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
       | term_of (TFree (x, S)) =
           if is_some (Term_Position.decode x) then Syntax.free x
           else ofsort (Syntax.const "_tfree" $ Syntax.free x) S
       | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S;
   in term_of ty end;
 
 
 (* simple_ast_of *)
 
 fun simple_ast_of ctxt =
   let
     val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
     fun ast_of (Const (c, _)) = Ast.Constant c
       | ast_of (Free (x, _)) = Ast.Variable x
       | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
       | ast_of (t as _ $ _) =
           let val (f, args) = strip_comb t
           in Ast.mk_appl (ast_of f) (map ast_of args) end
       | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
       | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
   in ast_of end;
 
 
 (* sort_to_ast and typ_to_ast *)
 
 fun ast_of_termT ctxt trf tm =
   let
     val ctxt' = Config.put show_sorts false ctxt;
     fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
       | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
       | ast_of (Const (a, _)) = trans a []
       | ast_of (t as _ $ _) =
           (case strip_comb t of
             (Const (a, _), args) => trans a args
           | (f, args) => Ast.Appl (map ast_of (f :: args)))
       | ast_of t = simple_ast_of ctxt t
     and trans a args = ast_of (trf a ctxt' dummyT args)
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   in ast_of tm end;
 
 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
 fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
 
 
 (* term_to_ast *)
 
 local
 
 fun mark_aprop tm =
   let
     fun aprop t = Syntax.const "_aprop" $ t;
 
     fun is_prop Ts t =
       Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT
         handle TERM _ => false;
 
     fun is_term (Const ("Pure.term", _) $ _) = true
       | is_term _ = false;
 
     fun mark _ (t as Const _) = t
       | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
       | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t
       | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
       | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
       | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
       | mark Ts (t as t1 $ (t2 as Const ("Pure.type", Type ("itself", [T])))) =
           if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
           else mark Ts t1 $ mark Ts t2
       | mark Ts (t as t1 $ t2) =
           (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop)
             (mark Ts t1 $ mark Ts t2);
   in mark [] tm end;
 
 fun prune_types tm =
   let
     fun regard t t' seen =
       if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
       else if member (op aconv) seen t then (t', seen)
       else (t, t :: seen);
 
     fun prune (t as Const _, seen) = (t, seen)
       | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen
       | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen
       | prune (t as Bound _, seen) = (t, seen)
       | prune (Abs (x, T, t), seen) =
           let val (t', seen') = prune (t, seen);
           in (Abs (x, T, t'), seen') end
       | prune (t1 $ t2, seen) =
           let
             val (t1', seen') = prune (t1, seen);
             val (t2', seen'') = prune (t2, seen');
           in (t1' $ t2', seen'') end;
   in #1 (prune (tm, [])) end;
 
 fun mark_atoms is_syntax_const ctxt tm =
   let
     val {structs, fixes} = Syntax_Trans.get_idents ctxt;
     val show_structs = Config.get ctxt show_structs;
 
     fun mark ((t as Const (c, _)) $ u) =
           if member (op =) Pure_Thy.token_markers c
           then t $ u else mark t $ mark u
       | mark (t $ u) = mark t $ mark u
       | mark (Abs (x, T, t)) = Abs (x, T, mark t)
       | mark (t as Const (c, T)) =
           if is_syntax_const c then t
           else Const (Lexicon.mark_const c, T)
       | mark (t as Free (x, T)) =
           let val i = find_index (fn s => s = x) structs + 1 in
             if i = 0 andalso member (op =) fixes x then
               Const (Lexicon.mark_fixed x, T)
             else if i = 1 andalso not show_structs then
               Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else Syntax.const "_free" $ t
           end
       | mark (t as Var (xi, T)) =
           if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
           else Syntax.const "_var" $ t
       | mark a = a;
   in mark tm end;
 
 in
 
 fun term_to_ast is_syntax_const ctxt trf tm =
   let
     val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
     val show_markup = Config.get ctxt show_markup;
 
     fun ast_of tm =
       (case strip_comb tm of
         (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
       | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
       | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
           let
             val X =
               if show_markup andalso not show_types orelse B <> dummyT then T
               else dummyT;
           in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
       | (Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
     and trans a T args = ast_of (trf a ctxt T args)
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T0 =
       let
         val T =
           if show_markup andalso not show_types
           then Type_Annotation.clean T0
           else Type_Annotation.smash T0;
       in
         if (show_types orelse show_markup) andalso T <> dummyT then
           Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
             ast_of_termT ctxt trf (term_of_typ ctxt T)]
         else simple_ast_of ctxt t
       end;
   in
     tm
     |> mark_aprop
     |> show_types ? prune_types
     |> Variable.revert_bounds ctxt
     |> mark_atoms is_syntax_const ctxt
     |> ast_of
   end;
 
 end;
 
 
 
 (** unparse **)
 
 local
 
 fun free_or_skolem ctxt x =
   let
     val m =
       if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
       then Markup.fixed x else Markup.intensify;
   in
     if Name.is_skolem x
     then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
     else ([m, Markup.free], x)
   end;
 
 fun var_or_skolem s =
   (case Lexicon.read_variable s of
     SOME (x, i) =>
       (case try Name.dest_skolem x of
         NONE => (Markup.var, s)
       | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
   | NONE => (Markup.var, s));
 
 val typing_elem = YXML.output_markup_elem Markup.typing;
 val sorting_elem = YXML.output_markup_elem Markup.sorting;
 
 fun unparse_t t_to_ast prt_t markup ctxt t =
   let
     val show_markup = Config.get ctxt show_markup;
     val show_sorts = Config.get ctxt show_sorts;
     val show_types = Config.get ctxt show_types orelse show_sorts;
 
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val prtabs = Syntax.prtabs syn;
     val trf = Syntax.print_ast_translation syn;
 
     fun markup_extern c =
       (case Syntax.lookup_const syn c of
         SOME "" => ([], c)
       | SOME b => markup_extern b
       | NONE => c |> Lexicon.unmark
          {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
           case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
           case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
           case_fixed = fn x => free_or_skolem ctxt x,
           case_default = fn x => ([], x)});
 
     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
       | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
       | token_trans _ _ = NONE;
 
     fun markup_trans a [Ast.Variable x] = token_trans a x
       | markup_trans "_constrain" [t, ty] = constrain_trans t ty
       | markup_trans "_idtyp" [t, ty] = constrain_trans t ty
       | markup_trans "_ofsort" [ty, s] = ofsort_trans ty s
       | markup_trans _ _ = NONE
 
     and constrain_trans t ty =
       if show_markup andalso not show_types then
         let
           val ((bg1, bg2), en) = typing_elem;
           val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_ast Markup.empty t]) end
       else NONE
 
     and ofsort_trans ty s =
       if show_markup andalso not show_sorts then
         let
           val ((bg1, bg2), en) = sorting_elem;
           val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
           val info = {markup = (bg, en), consistent = false, indent = 0};
         in SOME (Pretty.make_block info [pretty_typ_ast Markup.empty ty]) end
       else NONE
 
     and pretty_typ_ast m ast = ast
       |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
       |> Pretty.markup m
 
     and pretty_ast m ast = ast
       |> prt_t ctxt prtabs trf markup_trans markup_extern
       |> Pretty.markup m;
   in
     t_to_ast ctxt (Syntax.print_translation syn) t
     |> Ast.normalize ctxt (Syntax.print_rules syn)
     |> pretty_ast markup
   end;
 
 in
 
 val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
 val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
 
 fun unparse_term ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
   in
     unparse_t (term_to_ast (is_some o Syntax.lookup_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
       (Markup.language_term false) ctxt
   end;
 
 end;
 
 
 
 (** translations **)
 
 (* type propositions *)
 
 fun type_prop_tr' ctxt T [Const ("\<^const>Pure.sort_constraint", _)] =
       Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
   | type_prop_tr' ctxt T [t] =
       Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
   | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
 
 
 (* type reflection *)
 
 fun type_tr' ctxt (Type ("itself", [T])) ts =
       Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
   | type_tr' _ _ _ = raise Match;
 
 
 (* type constraints *)
 
 fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
       Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
   | type_constraint_tr' _ _ _ = raise Match;
 
 
 (* authentic syntax *)
 
 fun const_ast_tr intern ctxt asts =
   (case asts of
     [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
         val pos = the_default Position.none (Term_Position.decode p);
         val (c', _) = decode_const ctxt (c, [pos]);
         val d = if intern then Lexicon.mark_const c' else c;
       in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
   | _ => raise Ast.AST ("const_ast_tr", asts));
 
 
 (* setup translations *)
 
 val _ = Theory.setup
  (Sign.parse_ast_translation
    [("_context_const", const_ast_tr true),
     ("_context_xconst", const_ast_tr false)] #>
   Sign.typed_print_translation
    [("_type_prop", type_prop_tr'),
     ("\<^const>Pure.type", type_tr'),
     ("_type_constraint_", type_constraint_tr')]);
 
 
 
 (** check/uncheck **)
 
 (* context-sensitive (un)checking *)
 
 type key = int * bool;
 
 structure Checks = Generic_Data
 (
   type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
   type T =
     ((key * ((string * typ check) * stamp) list) list *
      (key * ((string * term check) * stamp) list) list);
   val empty = ([], []);
   fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
     (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
      AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
 );
 
 fun print_checks ctxt =
   let
     fun split_checks checks =
       List.partition (fn ((_, un), _) => not un) checks
       |> apply2 (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
           #> sort (int_ord o apply2 fst));
     fun pretty_checks kind checks =
       checks |> map (fn (i, names) => Pretty.block
         [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
           Pretty.brk 1, Pretty.strs names]);
 
     val (typs, terms) = Checks.get (Context.Proof ctxt);
     val (typ_checks, typ_unchecks) = split_checks typs;
     val (term_checks, term_unchecks) = split_checks terms;
   in
     pretty_checks "typ_checks" typ_checks @
     pretty_checks "term_checks" term_checks @
     pretty_checks "typ_unchecks" typ_unchecks @
     pretty_checks "term_unchecks" term_unchecks
   end |> Pretty.writeln_chunks;
 
 
 local
 
 fun context_check which (key: key) name f =
   Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
 
 fun simple_check eq f xs ctxt =
   let val xs' = f ctxt xs
   in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
 
 in
 
 fun typ_check' stage = context_check apfst (stage, false);
 fun term_check' stage = context_check apsnd (stage, false);
 fun typ_uncheck' stage = context_check apfst (stage, true);
 fun term_uncheck' stage = context_check apsnd (stage, true);
 
 fun typ_check key name f = typ_check' key name (simple_check (op =) f);
 fun term_check key name f = term_check' key name (simple_check (op aconv) f);
 fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f);
 fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f);
 
 end;
 
 
 local
 
 fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
 fun check_all fs = perhaps_apply (map check_stage fs);
 
 fun check which uncheck ctxt0 xs0 =
   let
     val funs = which (Checks.get (Context.Proof ctxt0))
       |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
       |> Library.sort (int_ord o apply2 fst) |> map snd
       |> not uncheck ? map rev;
   in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
 
 val apply_typ_check = check fst false;
 val apply_term_check = check snd false;
 val apply_typ_uncheck = check fst true;
 val apply_term_uncheck = check snd true;
 
 in
 
 fun check_typs ctxt raw_tys =
   let
     val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
     val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else ();
   in
     tys
     |> apply_typ_check ctxt
     |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
   end;
 
 fun check_terms ctxt raw_ts =
   let
     val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
     val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
 
     val tys = map (Logic.mk_type o snd) ps;
     val (ts', tys') = ts @ tys
       |> apply_term_check ctxt
       |> chop (length ts);
     val typing_report =
       fold2 (fn (pos, _) => fn ty =>
         if Position.is_reported pos then
           cons (Position.reported_text pos Markup.typing
             (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
         else I) ps tys' [];
 
     val _ =
       if Context_Position.reports_enabled ctxt
       then Output.report (sorting_report @ typing_report) else ();
   in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
 
 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
 
 val uncheck_typs = apply_typ_uncheck;
 val uncheck_terms = apply_term_uncheck;
 
 end;
 
 
 (* install operations *)
 
 val _ =
   Theory.setup
    (Syntax.install_operations
      {parse_sort = parse_sort,
       parse_typ = parse_typ,
       parse_term = parse_term false,
       parse_prop = parse_term true,
       unparse_sort = unparse_sort,
       unparse_typ = unparse_typ,
       unparse_term = unparse_term,
       check_typs = check_typs,
       check_terms = check_terms,
       check_props = check_props,
       uncheck_typs = uncheck_typs,
       uncheck_terms = uncheck_terms});
 
 end;
 
 
 (* standard phases *)
 
 val _ = Context.>>
  (Syntax_Phases.typ_check 0 "standard" Proof_Context.standard_typ_check #>
   Syntax_Phases.term_check 0 "standard"
     (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
   Syntax_Phases.term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
   Syntax_Phases.term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
diff --git a/src/Pure/sign.ML b/src/Pure/sign.ML
--- a/src/Pure/sign.ML
+++ b/src/Pure/sign.ML
@@ -1,554 +1,554 @@
 (*  Title:      Pure/sign.ML
     Author:     Lawrence C Paulson and Markus Wenzel
 
 Logical signature content: naming conventions, concrete syntax, type
 signature, polymorphic constants.
 *)
 
 signature SIGN =
 sig
   val change_begin: theory -> theory
   val change_end: theory -> theory
   val change_end_local: Proof.context -> Proof.context
   val change_check: theory -> theory
-  val syn_of: theory -> Syntax.syntax
+  val syntax_of: theory -> Syntax.syntax
   val tsig_of: theory -> Type.tsig
   val classes_of: theory -> Sorts.algebra
   val all_classes: theory -> class list
   val super_classes: theory -> class -> class list
   val minimize_sort: theory -> sort -> sort
   val complete_sort: theory -> sort -> sort
   val set_defsort: sort -> theory -> theory
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
   val inter_sort: theory -> sort * sort -> sort
   val witness_sorts: theory ->
     (typ * sort) list -> sort Ord_List.T ->
     (typ * sort) list * sort Ord_List.T
   val logical_types: theory -> string list
   val typ_instance: theory -> typ * typ -> bool
   val typ_equiv: theory -> typ * typ -> bool
   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
   val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
   val consts_of: theory -> Consts.T
   val the_const_constraint: theory -> string -> typ
   val const_type: theory -> string -> typ option
   val the_const_type: theory -> string -> typ
   val declared_tyname: theory -> string -> bool
   val declared_const: theory -> string -> bool
   val naming_of: theory -> Name_Space.naming
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
   val restore_naming: theory -> theory -> theory
   val inherit_naming: theory -> Proof.context -> Context.generic
   val full_name: theory -> binding -> string
   val full_name_path: theory -> string -> binding -> string
   val full_bname: theory -> bstring -> string
   val full_bname_path: theory -> string -> bstring -> string
   val full_name_pos: theory -> binding -> string * Position.T
   val const_monomorphic: theory -> string -> bool
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
   val mk_const: theory -> string * typ list -> term
   val class_space: theory -> Name_Space.T
   val type_space: theory -> Name_Space.T
   val const_space: theory -> Name_Space.T
   val intern_class: theory -> xstring -> string
   val intern_type: theory -> xstring -> string
   val intern_const: theory -> xstring -> string
   val type_alias: binding -> string -> theory -> theory
   val const_alias: binding -> string -> theory -> theory
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
   val certify_class: theory -> class -> class
   val certify_sort: theory -> sort -> sort
   val certify_typ: theory -> typ -> typ
   val certify_typ_mode: Type.mode -> theory -> typ -> typ
   val certify_flags: {prop: bool, normalize: bool} -> Context.generic -> Consts.T -> theory ->
     term -> term * typ
   val certify_term: theory -> term -> term * typ
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
   val no_frees: Proof.context -> term -> term
   val no_vars: Proof.context -> term -> term
   val add_type: Proof.context -> binding * int * mixfix -> theory -> theory
   val add_types_global: (binding * int * mixfix) list -> theory -> theory
   val add_nonterminals: Proof.context -> binding list -> theory -> theory
   val add_nonterminals_global: binding list -> theory -> theory
   val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
   val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
   val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory
   val add_consts: (binding * typ * mixfix) list -> theory -> theory
   val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
   val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
   val revert_abbrev: string -> string -> theory -> theory
   val add_const_constraint: string * typ option -> theory -> theory
   val primitive_class: binding * class list -> theory -> theory
   val primitive_classrel: class * class -> theory -> theory
   val primitive_arity: arity -> theory -> theory
   val parse_ast_translation:
     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   val parse_translation:
     (string * (Proof.context -> term list -> term)) list -> theory -> theory
   val print_translation:
     (string * (Proof.context -> term list -> term)) list -> theory -> theory
   val typed_print_translation:
     (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
   val print_ast_translation:
     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   val get_scope: theory -> Binding.scope option
   val new_scope: theory -> Binding.scope * theory
   val new_group: theory -> theory
   val reset_group: theory -> theory
   val add_path: string -> theory -> theory
   val root_path: theory -> theory
   val parent_path: theory -> theory
   val mandatory_path: string -> theory -> theory
   val qualified_path: bool -> binding -> theory -> theory
   val local_path: theory -> theory
   val init_naming: theory -> theory
   val private_scope: Binding.scope -> theory -> theory
   val private: Position.T -> theory -> theory
   val qualified_scope: Binding.scope -> theory -> theory
   val qualified: Position.T -> theory -> theory
   val concealed: theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
   val hide_const: bool -> string -> theory -> theory
 end
 
 structure Sign: SIGN =
 struct
 
 (** datatype sign **)
 
 datatype sign = Sign of
  {syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
   tsig: Type.tsig,              (*order-sorted signature of types*)
   consts: Consts.T};            (*polymorphic constants*)
 
 fun rep_sign (Sign args) = args;
 fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
 
 structure Data = Theory_Data'
 (
   type T = sign;
   val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
   fun merge args =
     let
       val context0 = Context.Theory (#1 (hd args));
       val syn' = Library.foldl1 Syntax.merge_syntax (map (#syn o rep_sign o #2) args);
       val tsig' = Library.foldl1 (Type.merge_tsig context0) (map (#tsig o rep_sign o #2) args);
       val consts' = Library.foldl1 Consts.merge (map (#consts o rep_sign o #2) args);
     in make_sign (syn', tsig', consts') end;
 );
 
 val rep_sg = rep_sign o Data.get;
 
 fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts)));
 
 fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
 fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
 fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
 
 
 (* linear change discipline *)
 
 fun change_base begin = map_sign (fn (syn, tsig, consts) =>
   (syn, Type.change_base begin tsig, Consts.change_base begin consts));
 
 val change_begin = change_base true;
 val change_end = change_base false;
 
 fun change_end_local ctxt =
   Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt;
 
 fun change_check thy =
   if can change_end thy
   then raise Fail "Unfinished linear change of theory content" else thy;
 
 
 (* syntax *)
 
-val syn_of = #syn o rep_sg;
+val syntax_of = #syn o rep_sg;
 
 
 (* type signature *)
 
 val tsig_of = #tsig o rep_sg;
 
 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
 val all_classes = Sorts.all_classes o classes_of;
 val super_classes = Sorts.super_classes o classes_of;
 val minimize_sort = Sorts.minimize_sort o classes_of;
 val complete_sort = Sorts.complete_sort o classes_of;
 
 val set_defsort = map_tsig o Type.set_defsort;
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;
 val of_sort = Type.of_sort o tsig_of;
 val inter_sort = Type.inter_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
 val logical_types = Type.logical_types o tsig_of;
 
 val typ_instance = Type.typ_instance o tsig_of;
 fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
 val typ_match = Type.typ_match o tsig_of;
 val typ_unify = Type.unify o tsig_of;
 
 
 (* polymorphic constants *)
 
 val consts_of = #consts o rep_sg;
 val the_const_constraint = Consts.the_constraint o consts_of;
 val the_const_type = Consts.the_const_type o consts_of;
 val const_type = try o the_const_type;
 val const_monomorphic = Consts.is_monomorphic o consts_of;
 val const_typargs = Consts.typargs o consts_of;
 val const_instance = Consts.instance o consts_of;
 
 fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts));
 
 fun declared_tyname ctxt c = can (Type.the_decl (tsig_of ctxt)) (c, Position.none);
 val declared_const = can o the_const_constraint;
 
 
 (* naming *)
 
 val naming_of = Name_Space.naming_of o Context.Theory;
 val map_naming = Context.theory_map o Name_Space.map_naming;
 val restore_naming = map_naming o K o naming_of;
 fun inherit_naming thy = Name_Space.map_naming (K (naming_of thy)) o Context.Proof;
 
 val full_name = Name_Space.full_name o naming_of;
 fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
 
 fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
 fun full_bname_path thy path = full_name_path thy path o Binding.name;
 
 fun full_name_pos thy b = (full_name thy b, Binding.default_pos_of b);
 
 
 
 (** name spaces **)
 
 val class_space = Type.class_space o tsig_of;
 val type_space = Type.type_space o tsig_of;
 val const_space = Consts.space_of o consts_of;
 
 val intern_class = Name_Space.intern o class_space;
 val intern_type = Name_Space.intern o type_space;
 val intern_const = Name_Space.intern o const_space;
 
 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
 
 
 
 (** certify entities **)    (*exception TYPE*)
 
 (* certify wrt. type signature *)
 
 val arity_number = Type.arity_number o tsig_of;
 fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy);
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
 fun certify_typ_mode mode = Type.certify_typ mode o tsig_of;
 val certify_typ = certify_typ_mode Type.mode_default;
 
 
 (* certify term/prop *)
 
 local
 
 fun type_check context tm =
   let
     fun err_appl bs t T u U =
       let
         val xs = map Free bs;           (*we do not rename here*)
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
         val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U;
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
       | typ_of (_, Free  (_, T)) = T
       | typ_of (_, Var (_, T)) = T
       | typ_of (bs, Bound i) = snd (nth bs i handle General.Subscript =>
           raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
       | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
       | typ_of (bs, t $ u) =
           let val T = typ_of (bs, t) and U = typ_of (bs, u) in
             (case T of
               Type ("fun", [T1, T2]) =>
                 if T1 = U then T2 else err_appl bs t T u U
             | _ => err_appl bs t T u U)
           end;
   in typ_of ([], tm) end;
 
 fun err msg = raise TYPE (msg, [], []);
 
 fun check_vars (t $ u) = (check_vars t; check_vars u)
   | check_vars (Abs (_, _, t)) = check_vars t
   | check_vars (Free (x, _)) =
       if Long_Name.is_qualified x then err ("Malformed variable: " ^ quote x) else ()
   | check_vars (Var (xi as (_, i), _)) =
       if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else ()
   | check_vars _ = ();
 
 in
 
 fun certify_flags {prop, normalize} context consts thy tm =
   let
     val tsig = tsig_of thy;
     fun check_term t =
       let
         val _ = check_vars t;
         val t' = Type.certify_types Type.mode_default tsig t;
         val T = type_check context t';
         val t'' = Consts.certify {normalize = normalize} context tsig consts t';
       in if prop andalso T <> propT then err "Term not of type prop" else (t'', T) end;
 
     val (tm1, ty1) = check_term tm;
     val tm' = Soft_Type_System.global_purge thy tm1;
     val (tm2, ty2) = if tm1 = tm' then (tm1, ty1) else check_term tm';
   in if tm = tm2 then (tm, ty2) else (tm2, ty2) end;
 
 fun certify_term thy =
   certify_flags {prop = false, normalize = true} (Context.Theory thy) (consts_of thy) thy;
 
 fun cert_term_abbrev thy =
   #1 o certify_flags {prop = false, normalize = false} (Context.Theory thy) (consts_of thy) thy;
 
 val cert_term = #1 oo certify_term;
 
 fun cert_prop thy =
   #1 o certify_flags {prop = true, normalize = true} (Context.Theory thy) (consts_of thy) thy;
 
 end;
 
 
 (* specifications *)
 
 fun no_variables kind add addT mk mkT ctxt tm =
   (case (add tm [], addT tm []) of
     ([], []) => tm
   | (frees, tfrees) => error (Pretty.string_of (Pretty.block
       (Pretty.str ("Illegal " ^ kind ^ " variable(s) in term:") :: Pretty.brk 1 ::
        Pretty.commas
         (map (Syntax.pretty_term ctxt o mk) frees @ map (Syntax.pretty_typ ctxt o mkT) tfrees)))));
 
 val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
 val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
 
 
 
 (** signature extension functions **)  (*exception ERROR/TYPE*)
 
 (* add type constructors *)
 
 fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) =>
   let
     val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx);
     val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn;
     val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig;
   in (syn', tsig', consts) end);
 
 fun add_types_global types thy =
   fold (add_type (Syntax.init_pretty_global thy)) types thy;
 
 
 (* add nonterminals *)
 
 fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) =>
   (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts));
 
 fun add_nonterminals_global ns thy =
   add_nonterminals (Syntax.init_pretty_global thy) ns thy;
 
 
 (* add type abbreviations *)
 
 fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) =>
   (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts));
 
 
 (* modify syntax *)
 
 fun gen_syntax parse_typ add mode args thy =
   let
     val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
     fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
   in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end;
 
 val syntax = gen_syntax (K I);
 val syntax_cmd = gen_syntax Syntax.read_typ;
 
 fun type_notation add mode args =
   let
     fun type_syntax (Type (c, args), mx) =
           SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx)
       | type_syntax _ = NONE;
   in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
 
 fun notation add mode args thy =
   let
     fun const_syntax (Const (c, _), mx) =
           (case try (Consts.type_scheme (consts_of thy)) c of
             SOME T => SOME (Lexicon.mark_const c, T, mx)
           | NONE => NONE)
       | const_syntax _ = NONE;
   in syntax add mode (map_filter const_syntax args) thy end;
 
 
 (* add constants *)
 
 local
 
 fun gen_add_consts prep_typ ctxt raw_args thy =
   let
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o prep_typ ctxt;
     fun prep (b, raw_T, mx) =
       let
         val c = full_name thy b;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ Binding.print b);
         val T' = Logic.varifyT_global T;
       in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
     val args = map prep raw_args;
   in
     thy
     |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
     |> syntax true Syntax.mode_default (map #2 args)
     |> pair (map #3 args)
   end;
 
 in
 
 fun add_consts args thy =
   #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
 
 fun add_consts_cmd args thy =
   #2 (gen_add_consts Syntax.read_typ (Proof_Context.init_global thy) args thy);
 
 fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx);
 fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
 
 end;
 
 
 (* abbreviations *)
 
 fun add_abbrev mode (b, raw_t) thy =  (* FIXME proper ctxt (?) *)
   let
     val ctxt = Syntax.init_pretty_global thy;
     val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
     val (res, consts') = consts_of thy
       |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t);
   in (res, thy |> map_consts (K consts')) end;
 
 fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
 
 
 (* add constraints *)
 
 fun add_const_constraint (c, opt_T) thy =
   let
     fun prepT raw_T =
       let val T = Logic.varifyT_global (Type.no_tvars (Term.no_dummyT (certify_typ thy raw_T)))
       in cert_term thy (Const (c, T)); T end
       handle TYPE (msg, _, _) => error msg;
   in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;
 
 
 (* primitive classes and arities *)
 
 fun primitive_class (bclass, classes) thy =
   thy
   |> map_sign (fn (syn, tsig, consts) =>
       let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
       in (syn, tsig', consts) end)
   |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
 fun primitive_classrel arg thy =
   thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg);
 
 fun primitive_arity arg thy =
   thy |> map_tsig (Type.add_arity (Context.Theory thy) arg);
 
 
 (* add translation functions *)
 
 local
 
 fun mk trs = map Syntax_Ext.mk_trfun trs;
 
 in
 
 fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], []));
 fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], []));
 fun print_translation tr's =
   map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []));
 fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, []));
 fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's));
 
 end;
 
 
 (* translation rules *)
 
 val add_trrules = map_syn o Syntax.update_trrules;
 val del_trrules = map_syn o Syntax.remove_trrules;
 
 
 (* naming *)
 
 val get_scope = Name_Space.get_scope o naming_of;
 
 fun new_scope thy =
   let
     val (scope, naming') = Name_Space.new_scope (naming_of thy);
     val thy' = map_naming (K naming') thy;
   in (scope, thy') end;
 
 val new_group = map_naming Name_Space.new_group;
 val reset_group = map_naming Name_Space.reset_group;
 
 val add_path = map_naming o Name_Space.add_path;
 val root_path = map_naming Name_Space.root_path;
 val parent_path = map_naming Name_Space.parent_path;
 val mandatory_path = map_naming o Name_Space.mandatory_path;
 val qualified_path = map_naming oo Name_Space.qualified_path;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy);
 
 fun init_naming thy =
   let
     val theory_naming = Name_Space.global_naming
       |> Name_Space.set_theory_long_name (Context.theory_long_name thy);
   in map_naming (K theory_naming) thy end;
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
 val qualified_scope = map_naming o Name_Space.qualified_scope;
 val qualified = map_naming o Name_Space.qualified;
 val concealed = map_naming Name_Space.concealed;
 
 
 (* hide names *)
 
 val hide_class = map_tsig oo Type.hide_class;
 val hide_type = map_tsig oo Type.hide_type;
 val hide_const = map_consts oo Consts.hide;
 
 end;
diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML
--- a/src/Pure/theory.ML
+++ b/src/Pure/theory.ML
@@ -1,397 +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)
+      |> tap (Syntax.cache_syntax o Sign.syntax_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;