src/Doc/IsarImplementation/ML.thy

--- a/src/Doc/IsarImplementation/ML.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -666,9 +666,9 @@
   concept of \emph{ML antiquotation}.  The standard token language of
   ML is augmented by special syntactic entities of the following form:
 
-  @{rail "
+  @{rail \<open>
   @{syntax_def antiquote}: '@{' nameref args '}'
-  "}
+  \<close>}
 
   Here @{syntax nameref} and @{syntax args} are regular outer syntax
   categories \cite{isabelle-isar-ref}.  Attributes and proof methods
@@ -699,9 +699,9 @@
   @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   @@{ML_antiquotation make_string}
-  "}
+  \<close>}
 
   \begin{description}