src/Pure/Isar/toplevel.ML

 fun proof_result immediate (tr, proof_trs) st =
   let val st' = command tr st in
     if immediate orelse
       null proof_trs orelse
       OuterKeyword.is_schematic_goal (name_of tr) orelse
+      exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
       not (can proof_of st') orelse
       Proof.is_relevant (proof_of st')
     then
       let val (states, st'') = fold_map command_result proof_trs st'
       in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end