src/Pure/Isar/proof.ML

     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
-  val future_terminal_proof: Method.text * Method.text option -> state -> context
+  val future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
 end;
 
 structure Proof: PROOF =
 struct
 

 
 in
 
 fun is_relevant state =
   can (assert_bottom false) state orelse
-  can assert_forward state orelse
   not (is_original state) orelse
   schematic_goal state;
 
 fun future_proof fork_proof state =
   let
     val _ = is_relevant state andalso error "Cannot fork relevant proof";
 
+    val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
     val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
 
     val prop' = Logic.protect prop;
     val statement' = (kind, [[], [prop']], prop');

       |> global_done_proof;
   in (Future.map #1 result_ctxt, state') end;
 
 end;
 
-fun future_terminal_proof meths state =
-  if is_relevant state orelse not (Future.enabled ()) then global_terminal_proof meths state
+fun future_terminal_proof meths int state =
+  if int orelse is_relevant state orelse not (Future.enabled ())
+  then global_terminal_proof meths state
   else #2 (state |> future_proof (fn state' =>
     Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
 
 end;