diff -r 78759a7bd874 -r e5ba0ca1e465 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Jan 15 22:46:04 2018 +0100
+++ b/src/Pure/Isar/token.ML	Mon Jan 15 23:03:01 2018 +0100
@@ -289,7 +289,7 @@
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
-  | Comment NONE => (Markup.comment, "")
+  | Comment _ => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");