src/Doc/Implementation/ML.thy
changeset 67146 909dcdec2122
parent 66663 49318345c332
child 67744 5c781dcd5864
     1.1 --- a/src/Doc/Implementation/ML.thy	Wed Dec 06 14:19:36 2017 +0100
     1.2 +++ b/src/Doc/Implementation/ML.thy	Wed Dec 06 15:46:35 2017 +0100
     1.3 @@ -695,7 +695,7 @@
     1.4    @{rail \<open>
     1.5    @@{ML_antiquotation make_string}
     1.6    ;
     1.7 -  @@{ML_antiquotation print} @{syntax name}?
     1.8 +  @@{ML_antiquotation print} embedded?
     1.9    \<close>}
    1.10  
    1.11    \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to