src/Pure/Thy/thy_output.ML

 
     val nesting = Toplevel.level state' - Toplevel.level state;
 
     val active_tag' =
       if is_some tag' then tag'
-      else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
+      else if cmd_name = "end" andalso Toplevel.is_end_theory state' then SOME "theory"
       else
         (case Keyword.command_tags keywords cmd_name @ document_tags of
           default_tag :: _ => SOME default_tag
         | [] =>
             if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state