diff -r 11417d1eff3b -r b68e1c27709a doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sun May 01 17:41:49 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun May 01 17:42:21 2011 +0200
@@ -699,9 +699,9 @@
   \end{matharray}
 
   @{rail "
-  @@{ML_antiquotation let} ((term + @@{keyword \"and\"}) '=' term + @@{keyword \"and\"})
+  @@{ML_antiquotation let} ((term + @'and') '=' term + @'and')
   ;
-  @@{ML_antiquotation note} (thmdef? thmrefs + @@{keyword \"and\"})
+  @@{ML_antiquotation note} (thmdef? thmrefs + @'and')
   "}
 
   \begin{description}