src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -713,6 +713,7 @@
   (case try proof_of st of
     NONE => false
   | SOME state =>
+      not (Proofterm.proofs_enabled ()) andalso
       not (Proof.is_relevant state) andalso
        (if can (Proof.assert_bottom true) state
         then Future.proofs_enabled 1