src/Pure/Isar/toplevel.ML

 
 fun timing_estimate elem =
   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)
       else command tr st;
   in (Result (tr, st'), st') end;

       let
         val (head_result, st') = atom_result keywords head_tr st;
         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];
             val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st';
           in (Result_List (head_result :: proof_results), st'') end