--- a/src/Pure/Isar/proof.ML Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jul 23 12:07:50 2019 +0200
@@ -1293,7 +1293,10 @@
local
fun future_terminal_proof proof1 proof2 done state =
- if Future.proofs_enabled 3 andalso not (is_relevant state) then
+ if Future.proofs_enabled 3 andalso
+ not (Proofterm.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}