--- a/src/Pure/Thy/thy_info.ML Fri Dec 08 15:03:54 2017 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Dec 08 16:02:44 2017 +0100
@@ -266,8 +266,7 @@
let
val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
in
- if exists (Toplevel.is_skipped_proof o #2) res then
- warning ("Cannot present theory with skipped proofs: " ^ quote name)
+ if exists (Toplevel.is_skipped_proof o #2) res then ()
else
let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
in if document then Present.theory_output thy tex_source else () end