# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 3e060b1c844b0d966855bb013ed41549baa4cab4
# Parent  1c451bbb3ad704f700fea69868c72be987b20315
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)

diff -r 1c451bbb3ad7 -r 3e060b1c844b src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:08 2011 +0200
@@ -44,7 +44,6 @@
 
   type 'a proof = ('a, 'a, 'a fo_term) formula step list
 
-  val serial_commas : string -> string list -> string list
   val strip_spaces : bool -> (char -> bool) -> string -> string
   val short_output : bool -> string -> string
   val string_for_failure : failure -> string
@@ -94,12 +93,6 @@
   InternalError |
   UnknownError of string
 
-fun serial_commas _ [] = ["??"]
-  | serial_commas _ [s] = [s]
-  | serial_commas conj [s1, s2] = [s1, conj, s2]
-  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
-  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-
 fun strip_c_style_comment _ [] = []
   | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
     strip_spaces_in_list true is_evil cs
@@ -149,7 +142,8 @@
 
 fun involving [] = ""
   | involving ss =
-    "involving " ^ space_implode " " (serial_commas "and" (map quote ss)) ^ " "
+    "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
+    " "
 
 fun string_for_failure Unprovable = "The problem is unprovable."
   | string_for_failure IncompleteUnprovable = "The prover gave up."
diff -r 1c451bbb3ad7 -r 3e060b1c844b src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri May 27 10:30:08 2011 +0200
@@ -226,7 +226,7 @@
 val plural_s = Sledgehammer_Util.plural_s
 fun plural_s_for_list xs = plural_s (length xs)
 
-val serial_commas = Sledgehammer_Util.serial_commas
+val serial_commas = Try.serial_commas
 
 fun pretty_serial_commas _ [] = []
   | pretty_serial_commas _ [p] = [p]
diff -r 1c451bbb3ad7 -r 3e060b1c844b src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 27 10:30:08 2011 +0200
@@ -32,7 +32,7 @@
 val implode_desc = op ^ o apfst quote
 
 fun implode_message (workers, work) =
-  space_implode " " (ATP_Proof.serial_commas "and" (map quote workers)) ^ work
+  space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work
 
 
 (* data structures over threads *)
diff -r 1c451bbb3ad7 -r 3e060b1c844b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
@@ -38,7 +38,7 @@
 
 fun plural_s n = if n = 1 then "" else "s"
 
-val serial_commas = ATP_Proof.serial_commas
+val serial_commas = Try.serial_commas
 val simplify_spaces = ATP_Proof.strip_spaces false (K true)
 
 fun parse_bool_option option name s =
@@ -231,7 +231,7 @@
     | NONE => raise Type.TYPE_MATCH
   end
 
-val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+val subgoal_count = Try.subgoal_count
 
 fun strip_subgoal ctxt goal i =
   let
diff -r 1c451bbb3ad7 -r 3e060b1c844b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
@@ -638,22 +638,22 @@
     | SOME results =>
         let
           val msg = pretty_counterex_and_reports ctxt auto results
-                    |> not auto ? tap (Output.urgent_message o Pretty.string_of)
         in
           if exists found_counterexample results then
             (genuineN,
-             state |> (if auto then
-                         Proof.goal_message (K (Pretty.chunks [Pretty.str "",
-                             Pretty.mark Markup.hilite msg]))
-                       else
-                         I))
+             state
+             |> (if auto then
+                   Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+                       Pretty.mark Markup.hilite msg]))
+                 else
+                   tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
           else
             (noneN, state)
         end
   end
   |> `(fn (outcome_code, _) => outcome_code = genuineN)
 
-val setup = Try.register_tool (quickcheckN, (30, auto, try_quickcheck))
+val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck))
 
 end;