src/Pure/Thy/thy_info.ML
changeset 67163 257bcd20eeec
parent 66873 9953ae603a23
child 67173 e746db6db903
     1.1 --- a/src/Pure/Thy/thy_info.ML	Fri Dec 08 15:03:54 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Dec 08 16:02:44 2017 +0100
     1.3 @@ -266,8 +266,7 @@
     1.4        let
     1.5          val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
     1.6        in
     1.7 -        if exists (Toplevel.is_skipped_proof o #2) res then
     1.8 -          warning ("Cannot present theory with skipped proofs: " ^ quote name)
     1.9 +        if exists (Toplevel.is_skipped_proof o #2) res then ()
    1.10          else
    1.11            let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
    1.12            in if document then Present.theory_output thy tex_source else () end