--- a/src/Doc/Implementation/Local_Theory.thy Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy Sat May 22 13:35:25 2021 +0200
@@ -90,7 +90,7 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_type local_theory: Proof.context} \\
+ @{index_ML_type local_theory = Proof.context} \\
@{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory"} \\