1.1 --- a/src/Pure/Isar/proof.ML	Wed Jan 07 12:08:22 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Jan 07 12:09:39 2009 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4      ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
     1.5    val is_relevant: state -> bool
     1.6    val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
     1.7 -  val future_terminal_proof: Method.text * Method.text option -> state -> context
     1.8 +  val future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
     1.9  end;
    1.10  
    1.11  structure Proof: PROOF =
    1.12 @@ -993,7 +993,6 @@
    1.13  
    1.14  fun is_relevant state =
    1.15    can (assert_bottom false) state orelse
    1.16 -  can assert_forward state orelse
    1.17    not (is_original state) orelse
    1.18    schematic_goal state;
    1.19  
    1.20 @@ -1001,6 +1000,7 @@
    1.21    let
    1.22      val _ = is_relevant state andalso error "Cannot fork relevant proof";
    1.23  
    1.24 +    val _ = assert_backward state;
    1.25      val (goal_ctxt, (_, goal)) = find_goal state;
    1.26      val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
    1.27  
    1.28 @@ -1028,8 +1028,9 @@
    1.29  
    1.30  end;
    1.31  
    1.32 -fun future_terminal_proof meths state =
    1.33 -  if is_relevant state orelse not (Future.enabled ()) then global_terminal_proof meths state
    1.34 +fun future_terminal_proof meths int state =
    1.35 +  if int orelse is_relevant state orelse not (Future.enabled ())
    1.36 +  then global_terminal_proof meths state
    1.37    else #2 (state |> future_proof (fn state' =>
    1.38      Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
    1.39