diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Syntax.thy
--- a/src/Doc/Implementation/Syntax.thy	Sat May 22 13:35:25 2021 +0200
+++ b/src/Doc/Implementation/Syntax.thy	Sat May 22 21:52:13 2021 +0200
@@ -69,16 +69,16 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Syntax.read_typs: "Proof.context -> string list -> typ list"} \\
-  @{index_ML Syntax.read_terms: "Proof.context -> string list -> term list"} \\
-  @{index_ML Syntax.read_props: "Proof.context -> string list -> term list"} \\[0.5ex]
-  @{index_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\
-  @{index_ML Syntax.read_term: "Proof.context -> string -> term"} \\
-  @{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\[0.5ex]
-  @{index_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\
-  @{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
-  @{index_ML Syntax.string_of_typ: "Proof.context -> typ -> string"} \\
-  @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
+  @{define_ML Syntax.read_typs: "Proof.context -> string list -> typ list"} \\
+  @{define_ML Syntax.read_terms: "Proof.context -> string list -> term list"} \\
+  @{define_ML Syntax.read_props: "Proof.context -> string list -> term list"} \\[0.5ex]
+  @{define_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\
+  @{define_ML Syntax.read_term: "Proof.context -> string -> term"} \\
+  @{define_ML Syntax.read_prop: "Proof.context -> string -> term"} \\[0.5ex]
+  @{define_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\
+  @{define_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\
+  @{define_ML Syntax.string_of_typ: "Proof.context -> typ -> string"} \\
+  @{define_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Syntax.read_typs\<close>~\<open>ctxt strs\<close> parses and checks a simultaneous list
@@ -158,11 +158,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
-  @{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
-  @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex]
-  @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
-  @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
+  @{define_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
+  @{define_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
+  @{define_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex]
+  @{define_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
+  @{define_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Syntax.parse_typ\<close>~\<open>ctxt str\<close> parses a source string as pre-type that
@@ -219,11 +219,11 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
-  @{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
-  @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex]
-  @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
-  @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
+  @{define_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
+  @{define_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
+  @{define_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex]
+  @{define_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
+  @{define_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Syntax.check_typs\<close>~\<open>ctxt Ts\<close> checks a simultaneous list of pre-types