src/Pure/Isar/outer_syntax.ML

   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) =>
     let
+      val keywords = Thy_Header.get_keywords thy;
       val command_tags = Parse.command_ -- Parse.tags;
-      val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
+      val tr0 =
+        Toplevel.empty
+        |> Toplevel.name name
+        |> Toplevel.position pos
+        |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
+        |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
     in
       (case lookup_commands thy name of
         SOME (Command {command_parser = Parser parse, ...}) =>
           Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
       | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>