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."