--- a/src/Pure/Isar/toplevel.ML Wed May 09 19:53:37 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed May 09 20:45:57 2018 +0200
@@ -668,19 +668,19 @@
let val trs = tl (Thy_Syntax.flat_element elem)
in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
-fun proof_future_enabled estimate st =
+fun future_proofs_enabled estimate st =
(case try proof_of st of
NONE => false
| SOME state =>
not (Proof.is_relevant state) andalso
(if can (Proof.assert_bottom true) state
- then Goal.future_enabled 1
- else Goal.future_enabled 2 orelse Goal.future_enabled_timing estimate));
+ then Future.proofs_enabled 1
+ else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate));
fun atom_result keywords tr st =
let
val st' =
- if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
+ if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
(Execution.fork
{name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
(fn () => command tr st); st)
@@ -696,7 +696,7 @@
val (body_elems, end_tr) = element_rest;
val estimate = timing_estimate elem;
in
- if not (proof_future_enabled estimate st')
+ if not (future_proofs_enabled estimate st')
then
let
val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];