| changeset 67440 | e5ba0ca1e465 |
| parent 67439 | 78759a7bd874 |
| child 67446 | 1f4d167b6ac9 |
--- 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, "");