diff -r b8e093f7a802 -r 90d760fa8f34 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jan 23 20:43:18 2018 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jan 24 11:56:38 2018 +0100
@@ -285,7 +285,7 @@
     if Keyword.is_command keywords name then
       let
         val markup =
-          Token.explode keywords Position.none name
+          Token.explode0 keywords name
           |> maps (command_reports thy)
           |> map (#2 o #1);
         val _ = Context_Position.reports ctxt (map (pair pos) markup);