diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Implementation/ML.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -578,7 +578,7 @@
   ML_prf %"ML" \<open>val a = 1\<close>
   {
     ML_prf %"ML" \<open>val b = a + 1\<close>
-  } -- \<open>Isar block structure ignored by ML environment\<close>
+  } \<comment> \<open>Isar block structure ignored by ML environment\<close>
   ML_prf %"ML" \<open>val c = b + 1\<close>
 end