src/Pure/Syntax/syntax_phases.ML

 
 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,

 
 (* 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);
 

 
   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)

 
 (* 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);

   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

 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;