src/Doc/Implementation/Logic.thy
changeset 67146 909dcdec2122
parent 65446 ed18feb34c07
child 68540 000a0e062529
--- 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 + ',') ')')?
   ;