1.1 --- a/src/Pure/Isar/proof.ML	Wed Feb 20 00:00:42 2013 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Feb 20 11:40:30 2013 +0100
     1.3 @@ -114,6 +114,7 @@
     1.4    val show_cmd: Method.text option -> (thm list list -> state -> state) ->
     1.5      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
     1.6    val schematic_goal: state -> bool
     1.7 +  val is_relevant: state -> bool
     1.8    val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
     1.9    val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
    1.10    val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->

     2.1 --- a/src/Pure/Isar/toplevel.ML	Wed Feb 20 00:00:42 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Feb 20 11:40:30 2013 +0100
     2.3 @@ -694,7 +694,8 @@
     2.4  
     2.5  fun proof_result immediate (tr, proof_trs) st =
     2.6    let val st' = command tr st in
     2.7 -    if immediate orelse null proof_trs orelse not (can proof_of st')
     2.8 +    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
     2.9 +      Proof.is_relevant (proof_of st')
    2.10      then
    2.11        let val (results, st'') = fold_map command_result proof_trs st'
    2.12        in (Future.value ((tr, st') :: results), st'') end