src/Pure/Isar/toplevel.ML
changeset 51226 1973089f1dba
parent 51222 8c3e5fb41139
child 51228 dff3471dd8bc
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Feb 20 00:00:42 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Feb 20 11:40:30 2013 +0100
     1.3 @@ -694,7 +694,8 @@
     1.4  
     1.5  fun proof_result immediate (tr, proof_trs) st =
     1.6    let val st' = command tr st in
     1.7 -    if immediate orelse null proof_trs orelse not (can proof_of st')
     1.8 +    if immediate orelse null proof_trs orelse not (can proof_of st') orelse
     1.9 +      Proof.is_relevant (proof_of st')
    1.10      then
    1.11        let val (results, st'') = fold_map command_result proof_trs st'
    1.12        in (Future.value ((tr, st') :: results), st'') end