src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Isar/proof.ML	Wed May 09 20:45:57 2018 +0200
@@ -1301,7 +1301,7 @@
 local
 
 fun future_terminal_proof proof1 proof2 done state =
-  if Goal.future_enabled 3 andalso not (is_relevant state) then
+  if Future.proofs_enabled 3 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}