--- a/src/Doc/Implementation/Logic.thy Wed Dec 06 14:19:36 2017 +0100
+++ b/src/Doc/Implementation/Logic.thy Wed Dec 06 15:46:35 2017 +0100
@@ -171,13 +171,13 @@
\end{matharray}
@{rail \<open>
- @@{ML_antiquotation class} name
+ @@{ML_antiquotation class} embedded
;
@@{ML_antiquotation sort} sort
;
(@@{ML_antiquotation type_name} |
@@{ML_antiquotation type_abbrev} |
- @@{ML_antiquotation nonterminal}) name
+ @@{ML_antiquotation nonterminal}) embedded
;
@@{ML_antiquotation typ} type
\<close>}
@@ -392,7 +392,7 @@
@{rail \<open>
(@@{ML_antiquotation const_name} |
- @@{ML_antiquotation const_abbrev}) name
+ @@{ML_antiquotation const_abbrev}) embedded
;
@@{ML_antiquotation const} ('(' (type + ',') ')')?
;