src/Pure/goal.ML

--- a/src/Pure/goal.ML	Mon Jul 22 21:55:02 2019 +0200
+++ b/src/Pure/goal.ML	Tue Jul 23 12:07:50 2019 +0200
@@ -165,7 +165,7 @@
 
     val schematic = exists is_schematic props;
     val immediate = is_none fork_pri;
-    val future = Future.proofs_enabled 1;
+    val future = Future.proofs_enabled 1 andalso not (Proofterm.proofs_enabled ());
     val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();