src/Pure/Isar/toplevel.ML
changeset 51322 fd67b7f219e4
parent 51321 75682dfff630
child 51323 1b37556a3644
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:23:06 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:43:57 2013 +0100
     1.3 @@ -735,15 +735,15 @@
     1.4      val proof_trs =
     1.5        (case opt_proof of
     1.6          NONE => []
     1.7 -      | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
     1.8 +      | SOME (a, b) => maps Thy_Syntax.flat_element a @ [b]);
     1.9  
    1.10      val (_, st') = atom_result head_tr st;
    1.11    in
    1.12 -    if not (Goal.future_enabled ()) orelse is_ignored head_tr orelse
    1.13 -      null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    1.14 +    if not (Goal.future_enabled ()) orelse null proof_trs orelse
    1.15 +      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    1.16      then
    1.17        let val (results, st'') = fold_map atom_result proof_trs st'
    1.18 -      in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
    1.19 +      in (Future.value ((head_tr, st') :: results), st'') end
    1.20      else
    1.21        let
    1.22          val (body_trs, end_tr) = split_last proof_trs;