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;

     2.1 --- a/src/Pure/Thy/thy_load.ML	Sun Mar 03 13:23:06 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Mar 03 13:43:57 2013 +0100
     2.3 @@ -265,7 +265,7 @@
     2.4          let val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax () in
     2.5            Thy_Output.present_thy minor Keyword.command_tags
     2.6              (Outer_Syntax.is_markup outer_syntax)
     2.7 -            (maps Future.join results) toks
     2.8 +            (filter_out (Toplevel.is_ignored o #1) (maps Future.join results)) toks
     2.9            |> Buffer.content
    2.10            |> Present.theory_output name
    2.11          end);