diff -r 66ce07e8dbf2 -r 1368cfa92b7a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Dec 04 23:10:52 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Dec 05 14:03:10 2017 +0100
@@ -183,10 +183,10 @@
   Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
 
 fun parse_command thy =
-  Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
+  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     let
       val keywords = Thy_Header.get_keywords thy;
-      val command_tags = Parse.command_ -- Parse.tags;
+      val command_tags = Parse.command -- Parse.tags;
       val tr0 =
         Toplevel.empty
         |> Toplevel.name name