# HG changeset patch
# User blanchet
# Date 1304338209 -7200
# Node ID b5e94b70bc06fe89a968bd8607e41e389f9e531c
# Parent  6ef61823b63ba03a5947c720267792384be3aa30
fixed random number invocation

diff -r 6ef61823b63b -r b5e94b70bc06 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 13:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 14:10:09 2011 +0200
@@ -337,7 +337,7 @@
 val atp_blacklist_max_iters = 10
 (* Important messages are important but not so important that users want to see
    them each time. *)
-val atp_important_message_keep_factor = 0.1
+val atp_important_message_keep_quotient = 10
 
 val fallback_best_type_systems =
   [Preds (Polymorphic, Const_Arg_Types), Many_Typed]
@@ -567,7 +567,8 @@
          (output, msecs, atp_proof, outcome)) =
       with_path cleanup export run_on problem_path_name
     val important_message =
-      if not auto andalso random () <= atp_important_message_keep_factor then
+      if not auto andalso
+         random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
         extract_important_message output
       else
         ""