diff -r c7866e763e9f -r e69f00f4b897 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 11 21:33:21 2019 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Apr 12 17:09:21 2019 +0200
@@ -233,7 +233,7 @@
         |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
         |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
       val command_markers =
-        Parse.command |-- Document_Source.tags >>
+        Parse.command |-- Document_Source.old_tags >>
           (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0);
     in
       (case lookup_commands thy name of