# HG changeset patch
# User blanchet
# Date 1314967400 -7200
# Node ID 3d7b737d200af70cd14552dd50a0c455e312a6ef
# Parent  897f32a827f29f8fe1354588bf2b5831ebc44d55
fewer TPTP important messages

diff -r 897f32a827f2 -r 3d7b737d200a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Sep 01 10:41:19 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 02 14:43:20 2011 +0200
@@ -505,7 +505,7 @@
 
 (* Important messages are important but not so important that users want to see
    them each time. *)
-val atp_important_message_keep_quotient = 10
+val atp_important_message_keep_quotient = 25
 
 fun choose_type_enc soundness best_type_enc format =
   the_default best_type_enc