src/Pure/Isar/proof.ML

 
 local
 
 fun future_terminal_proof proof1 proof2 done state =
   if Future.proofs_enabled 3 andalso
-    not (Proofterm.proofs_enabled ()) andalso
+    not (Proofterm.any_proofs_enabled ()) andalso
     not (is_relevant state)
   then
     state |> future_proof (fn state' =>
       let val pos = Position.thread_data () in
         Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}