# HG changeset patch
# User wenzelm
# Date 1512745364 -3600
# Node ID 257bcd20eeecdb154d55fb14b06aa15810ba4984
# Parent  0050cd50936db315012de5f13a2f04e818f6451c
removed somewhat pointless warning;

diff -r 0050cd50936d -r 257bcd20eeec src/Pure/Thy/thy_info.ML
--- 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