diff -r c8a2755bf220 -r ff784d5a5bfb src/Doc/Implementation/Syntax.thy
--- a/src/Doc/Implementation/Syntax.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/Doc/Implementation/Syntax.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -81,46 +81,43 @@
   @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
   \end{mldecls}
 
-  \<^descr> @{ML Syntax.read_typs}~\<open>ctxt strs\<close> parses and checks a simultaneous list
+  \<^descr> \<^ML>\<open>Syntax.read_typs\<close>~\<open>ctxt strs\<close> parses and checks a simultaneous list
   of source strings as types of the logic.
 
-  \<^descr> @{ML Syntax.read_terms}~\<open>ctxt strs\<close> parses and checks a simultaneous list
+  \<^descr> \<^ML>\<open>Syntax.read_terms\<close>~\<open>ctxt strs\<close> parses and checks a simultaneous list
   of source strings as terms of the logic. Type-reconstruction puts all parsed
   terms into the same scope: types of free variables ultimately need to
   coincide.
 
   If particular type-constraints are required for some of the arguments, the
   read operations needs to be split into its parse and check phases. Then it
-  is possible to use @{ML Type.constraint} on the intermediate pre-terms
+  is possible to use \<^ML>\<open>Type.constraint\<close> on the intermediate pre-terms
   (\secref{sec:term-check}).
 
-  \<^descr> @{ML Syntax.read_props}~\<open>ctxt strs\<close> parses and checks a simultaneous list
+  \<^descr> \<^ML>\<open>Syntax.read_props\<close>~\<open>ctxt strs\<close> parses and checks a simultaneous list
   of source strings as terms of the logic, with an implicit type-constraint
-  for each argument to enforce type @{typ prop}; this also affects the inner
-  syntax for parsing. The remaining type-reconstruction works as for @{ML
-  Syntax.read_terms}.
+  for each argument to enforce type \<^typ>\<open>prop\<close>; this also affects the inner
+  syntax for parsing. The remaining type-reconstruction works as for \<^ML>\<open>Syntax.read_terms\<close>.
 
-  \<^descr> @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop} are
+  \<^descr> \<^ML>\<open>Syntax.read_typ\<close>, \<^ML>\<open>Syntax.read_term\<close>, \<^ML>\<open>Syntax.read_prop\<close> are
   like the simultaneous versions, but operate on a single argument only. This
   convenient shorthand is adequate in situations where a single item in its
-  own scope is processed. Do not use @{ML "map o Syntax.read_term"} where @{ML
-  Syntax.read_terms} is actually intended!
+  own scope is processed. Do not use \<^ML>\<open>map o Syntax.read_term\<close> where \<^ML>\<open>Syntax.read_terms\<close> is actually intended!
 
-  \<^descr> @{ML Syntax.pretty_typ}~\<open>ctxt T\<close> and @{ML Syntax.pretty_term}~\<open>ctxt t\<close>
+  \<^descr> \<^ML>\<open>Syntax.pretty_typ\<close>~\<open>ctxt T\<close> and \<^ML>\<open>Syntax.pretty_term\<close>~\<open>ctxt t\<close>
   uncheck and pretty-print the given type or term, respectively. Although the
   uncheck phase acts on a simultaneous list as well, this is rarely used in
   practice, so only the singleton case is provided as combined pretty
   operation. There is no distinction of term vs.\ proposition.
 
-  \<^descr> @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are convenient
-  compositions of @{ML Syntax.pretty_typ} and @{ML Syntax.pretty_term} with
-  @{ML Pretty.string_of} for output. The result may be concatenated with other
+  \<^descr> \<^ML>\<open>Syntax.string_of_typ\<close> and \<^ML>\<open>Syntax.string_of_term\<close> are convenient
+  compositions of \<^ML>\<open>Syntax.pretty_typ\<close> and \<^ML>\<open>Syntax.pretty_term\<close> with
+  \<^ML>\<open>Pretty.string_of\<close> for output. The result may be concatenated with other
   strings, as long as there is no further formatting and line-breaking
   involved.
 
 
-  @{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML
-  Syntax.string_of_term} are the most important operations in practice.
+  \<^ML>\<open>Syntax.read_term\<close>, \<^ML>\<open>Syntax.read_prop\<close>, and \<^ML>\<open>Syntax.string_of_term\<close> are the most important operations in practice.
 
   \<^medskip>
   Note that the string values that are passed in and out are annotated by the
@@ -130,8 +127,8 @@
   datatype, encoded as concrete string for historical reasons.
 
   The standard way to provide the required position markup for input works via
-  the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already
-  part of @{ML Parse.typ}, @{ML Parse.term}, @{ML Parse.prop}. So a string
+  the outer syntax parser wrapper \<^ML>\<open>Parse.inner_syntax\<close>, which is already
+  part of \<^ML>\<open>Parse.typ\<close>, \<^ML>\<open>Parse.term\<close>, \<^ML>\<open>Parse.prop\<close>. So a string
   obtained from one of the latter may be directly passed to the corresponding
   read operation: this yields PIDE markup of the input and precise positions
   for warning and error messages.
@@ -168,27 +165,26 @@
   @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
   \end{mldecls}
 
-  \<^descr> @{ML Syntax.parse_typ}~\<open>ctxt str\<close> parses a source string as pre-type that
+  \<^descr> \<^ML>\<open>Syntax.parse_typ\<close>~\<open>ctxt str\<close> parses a source string as pre-type that
   is ready to be used with subsequent check operations.
 
-  \<^descr> @{ML Syntax.parse_term}~\<open>ctxt str\<close> parses a source string as pre-term that
+  \<^descr> \<^ML>\<open>Syntax.parse_term\<close>~\<open>ctxt str\<close> parses a source string as pre-term that
   is ready to be used with subsequent check operations.
 
-  \<^descr> @{ML Syntax.parse_prop}~\<open>ctxt str\<close> parses a source string as pre-term that
+  \<^descr> \<^ML>\<open>Syntax.parse_prop\<close>~\<open>ctxt str\<close> parses a source string as pre-term that
   is ready to be used with subsequent check operations. The inner syntax
-  category is @{typ prop} and a suitable type-constraint is included to ensure
+  category is \<^typ>\<open>prop\<close> and a suitable type-constraint is included to ensure
   that this information is observed in subsequent type reconstruction.
 
-  \<^descr> @{ML Syntax.unparse_typ}~\<open>ctxt T\<close> unparses a type after uncheck
+  \<^descr> \<^ML>\<open>Syntax.unparse_typ\<close>~\<open>ctxt T\<close> unparses a type after uncheck
   operations, to turn it into a pretty tree.
 
-  \<^descr> @{ML Syntax.unparse_term}~\<open>ctxt T\<close> unparses a term after uncheck
+  \<^descr> \<^ML>\<open>Syntax.unparse_term\<close>~\<open>ctxt T\<close> unparses a term after uncheck
   operations, to turn it into a pretty tree. There is no distinction for
   propositions here.
 
 
-  These operations always operate on a single item; use the combinator @{ML
-  map} to apply them to a list.
+  These operations always operate on a single item; use the combinator \<^ML>\<open>map\<close> to apply them to a list.
 \<close>
 
 
@@ -230,36 +226,34 @@
   @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
   \end{mldecls}
 
-  \<^descr> @{ML Syntax.check_typs}~\<open>ctxt Ts\<close> checks a simultaneous list of pre-types
+  \<^descr> \<^ML>\<open>Syntax.check_typs\<close>~\<open>ctxt Ts\<close> checks a simultaneous list of pre-types
   as types of the logic. Typically, this involves normalization of type
   synonyms.
 
-  \<^descr> @{ML Syntax.check_terms}~\<open>ctxt ts\<close> checks a simultaneous list of pre-terms
+  \<^descr> \<^ML>\<open>Syntax.check_terms\<close>~\<open>ctxt ts\<close> checks a simultaneous list of pre-terms
   as terms of the logic. Typically, this involves type-inference and
   normalization term abbreviations. The types within the given terms are
-  treated in the same way as for @{ML Syntax.check_typs}.
+  treated in the same way as for \<^ML>\<open>Syntax.check_typs\<close>.
 
   Applications sometimes need to check several types and terms together. The
-  standard approach uses @{ML Logic.mk_type} to embed the language of types
+  standard approach uses \<^ML>\<open>Logic.mk_type\<close> to embed the language of types
   into that of terms; all arguments are appended into one list of terms that
-  is checked; afterwards the type arguments are recovered with @{ML
-  Logic.dest_type}.
+  is checked; afterwards the type arguments are recovered with \<^ML>\<open>Logic.dest_type\<close>.
 
-  \<^descr> @{ML Syntax.check_props}~\<open>ctxt ts\<close> checks a simultaneous list of pre-terms
-  as terms of the logic, such that all terms are constrained by type @{typ
-  prop}. The remaining check operation works as @{ML Syntax.check_terms}
+  \<^descr> \<^ML>\<open>Syntax.check_props\<close>~\<open>ctxt ts\<close> checks a simultaneous list of pre-terms
+  as terms of the logic, such that all terms are constrained by type \<^typ>\<open>prop\<close>. The remaining check operation works as \<^ML>\<open>Syntax.check_terms\<close>
   above.
 
-  \<^descr> @{ML Syntax.uncheck_typs}~\<open>ctxt Ts\<close> unchecks a simultaneous list of types
+  \<^descr> \<^ML>\<open>Syntax.uncheck_typs\<close>~\<open>ctxt Ts\<close> unchecks a simultaneous list of types
   of the logic, in preparation of pretty printing.
 
-  \<^descr> @{ML Syntax.uncheck_terms}~\<open>ctxt ts\<close> unchecks a simultaneous list of terms
+  \<^descr> \<^ML>\<open>Syntax.uncheck_terms\<close>~\<open>ctxt ts\<close> unchecks a simultaneous list of terms
   of the logic, in preparation of pretty printing. There is no distinction for
   propositions here.
 
 
   These operations always operate simultaneously on a list; use the combinator
-  @{ML singleton} to apply them to a single item.
+  \<^ML>\<open>singleton\<close> to apply them to a single item.
 \<close>
 
 end