src/Doc/Isar_Ref/Inner_Syntax.thy
changeset 67146 909dcdec2122
parent 63933 e149e3e320a3
child 67352 5f7f339f3d7e
     1.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Dec 06 14:19:36 2017 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Dec 06 15:46:35 2017 +0100
     1.3 @@ -1307,7 +1307,7 @@
     1.4    (@@{ML_antiquotation class_syntax} |
     1.5     @@{ML_antiquotation type_syntax} |
     1.6     @@{ML_antiquotation const_syntax} |
     1.7 -   @@{ML_antiquotation syntax_const}) name
     1.8 +   @@{ML_antiquotation syntax_const}) embedded
     1.9    \<close>}
    1.10  
    1.11    \<^descr> @{command parse_translation} etc. declare syntax translation functions to