1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -44,7 +44,6 @@
     1.4  
     1.5    type 'a proof = ('a, 'a, 'a fo_term) formula step list
     1.6  
     1.7 -  val serial_commas : string -> string list -> string list
     1.8    val strip_spaces : bool -> (char -> bool) -> string -> string
     1.9    val short_output : bool -> string -> string
    1.10    val string_for_failure : failure -> string
    1.11 @@ -94,12 +93,6 @@
    1.12    InternalError |
    1.13    UnknownError of string
    1.14  
    1.15 -fun serial_commas _ [] = ["??"]
    1.16 -  | serial_commas _ [s] = [s]
    1.17 -  | serial_commas conj [s1, s2] = [s1, conj, s2]
    1.18 -  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    1.19 -  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    1.20 -
    1.21  fun strip_c_style_comment _ [] = []
    1.22    | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
    1.23      strip_spaces_in_list true is_evil cs
    1.24 @@ -149,7 +142,8 @@
    1.25  
    1.26  fun involving [] = ""
    1.27    | involving ss =
    1.28 -    "involving " ^ space_implode " " (serial_commas "and" (map quote ss)) ^ " "
    1.29 +    "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
    1.30 +    " "
    1.31  
    1.32  fun string_for_failure Unprovable = "The problem is unprovable."
    1.33    | string_for_failure IncompleteUnprovable = "The prover gave up."

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri May 27 10:30:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri May 27 10:30:08 2011 +0200
     2.3 @@ -226,7 +226,7 @@
     2.4  val plural_s = Sledgehammer_Util.plural_s
     2.5  fun plural_s_for_list xs = plural_s (length xs)
     2.6  
     2.7 -val serial_commas = Sledgehammer_Util.serial_commas
     2.8 +val serial_commas = Try.serial_commas
     2.9  
    2.10  fun pretty_serial_commas _ [] = []
    2.11    | pretty_serial_commas _ [p] = [p]

     3.1 --- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 27 10:30:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Fri May 27 10:30:08 2011 +0200
     3.3 @@ -32,7 +32,7 @@
     3.4  val implode_desc = op ^ o apfst quote
     3.5  
     3.6  fun implode_message (workers, work) =
     3.7 -  space_implode " " (ATP_Proof.serial_commas "and" (map quote workers)) ^ work
     3.8 +  space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work
     3.9  
    3.10  
    3.11  (* data structures over threads *)

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
     4.3 @@ -38,7 +38,7 @@
     4.4  
     4.5  fun plural_s n = if n = 1 then "" else "s"
     4.6  
     4.7 -val serial_commas = ATP_Proof.serial_commas
     4.8 +val serial_commas = Try.serial_commas
     4.9  val simplify_spaces = ATP_Proof.strip_spaces false (K true)
    4.10  
    4.11  fun parse_bool_option option name s =
    4.12 @@ -231,7 +231,7 @@
    4.13      | NONE => raise Type.TYPE_MATCH
    4.14    end
    4.15  
    4.16 -val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
    4.17 +val subgoal_count = Try.subgoal_count
    4.18  
    4.19  fun strip_subgoal ctxt goal i =
    4.20    let

     5.1 --- a/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     5.2 +++ b/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     5.3 @@ -638,22 +638,22 @@
     5.4      | SOME results =>
     5.5          let
     5.6            val msg = pretty_counterex_and_reports ctxt auto results
     5.7 -                    |> not auto ? tap (Output.urgent_message o Pretty.string_of)
     5.8          in
     5.9            if exists found_counterexample results then
    5.10              (genuineN,
    5.11 -             state |> (if auto then
    5.12 -                         Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    5.13 -                             Pretty.mark Markup.hilite msg]))
    5.14 -                       else
    5.15 -                         I))
    5.16 +             state
    5.17 +             |> (if auto then
    5.18 +                   Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    5.19 +                       Pretty.mark Markup.hilite msg]))
    5.20 +                 else
    5.21 +                   tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
    5.22            else
    5.23              (noneN, state)
    5.24          end
    5.25    end
    5.26    |> `(fn (outcome_code, _) => outcome_code = genuineN)
    5.27  
    5.28 -val setup = Try.register_tool (quickcheckN, (30, auto, try_quickcheck))
    5.29 +val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck))
    5.30  
    5.31  end;
    5.32