src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 07 16:59:12 2019 +0000
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 08 17:05:23 2019 +0100
@@ -185,7 +185,7 @@
   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 -- Document_Source.tags;
       val tr0 =
         Toplevel.empty
         |> Toplevel.name name