src/Pure/Isar/toplevel.ML
changeset 68132 6fb85346cb79
parent 67932 04352338f7f3
child 68505 088780aa2b70
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed May 09 19:53:37 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed May 09 20:45:57 2018 +0200
     1.3 @@ -668,19 +668,19 @@
     1.4    let val trs = tl (Thy_Syntax.flat_element elem)
     1.5    in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
     1.6  
     1.7 -fun proof_future_enabled estimate st =
     1.8 +fun future_proofs_enabled estimate st =
     1.9    (case try proof_of st of
    1.10      NONE => false
    1.11    | SOME state =>
    1.12        not (Proof.is_relevant state) andalso
    1.13         (if can (Proof.assert_bottom true) state
    1.14 -        then Goal.future_enabled 1
    1.15 -        else Goal.future_enabled 2 orelse Goal.future_enabled_timing estimate));
    1.16 +        then Future.proofs_enabled 1
    1.17 +        else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate));
    1.18  
    1.19  fun atom_result keywords tr st =
    1.20    let
    1.21      val st' =
    1.22 -      if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
    1.23 +      if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
    1.24          (Execution.fork
    1.25            {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
    1.26            (fn () => command tr st); st)
    1.27 @@ -696,7 +696,7 @@
    1.28          val (body_elems, end_tr) = element_rest;
    1.29          val estimate = timing_estimate elem;
    1.30        in
    1.31 -        if not (proof_future_enabled estimate st')
    1.32 +        if not (future_proofs_enabled estimate st')
    1.33          then
    1.34            let
    1.35              val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];