src/Pure/Isar/proof.ML
changeset 51605 eca8acb42e4a
parent 51584 98029ceda8ce
child 51606 2843cc095a57
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Apr 03 20:56:08 2013 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Apr 03 21:30:32 2013 +0200
     1.3 @@ -1158,24 +1158,23 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun future_terminal_proof n proof1 proof2 done int state =
     1.8 -  if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
     1.9 -    andalso not (is_relevant state)
    1.10 -  then
    1.11 +fun future_terminal_proof proof1 proof2 done int state =
    1.12 +  if Goal.future_enabled_level 3 andalso not (is_relevant state) then
    1.13      state |> future_proof (fn state' =>
    1.14 -      Goal.fork_name "Proof.future_terminal_proof" ~1
    1.15 +      Goal.fork_params
    1.16 +        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
    1.17          (fn () => ((), proof2 state'))) |> snd |> done
    1.18    else proof1 state;
    1.19  
    1.20  in
    1.21  
    1.22  fun local_future_terminal_proof meths =
    1.23 -  future_terminal_proof 3
    1.24 +  future_terminal_proof
    1.25      (local_terminal_proof meths)
    1.26      (local_terminal_proof meths #> context_of) local_done_proof;
    1.27  
    1.28  fun global_future_terminal_proof meths =
    1.29 -  future_terminal_proof 3
    1.30 +  future_terminal_proof
    1.31      (global_terminal_proof meths)
    1.32      (global_terminal_proof meths) global_done_proof;
    1.33