src/HOL/Tools/Nitpick/nitpick_util.ML
changeset 35962 77f2cb359b49
parent 35866 513074557e06
child 36380 1e8fcaccb3e8
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Mar 23 11:39:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Mar 23 11:40:46 2010 +0100
     1.3 @@ -46,7 +46,6 @@
     1.4    val triple_lookup :
     1.5      (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
     1.6    val is_substring_of : string -> string -> bool
     1.7 -  val serial_commas : string -> string list -> string list
     1.8    val plural_s : int -> string
     1.9    val plural_s_for_list : 'a list -> string
    1.10    val flip_polarity : polarity -> polarity
    1.11 @@ -233,13 +232,6 @@
    1.12    not (Substring.isEmpty (snd (Substring.position needle
    1.13                                                    (Substring.full stack))))
    1.14  
    1.15 -(* string -> string list -> string list *)
    1.16 -fun serial_commas _ [] = ["??"]
    1.17 -  | serial_commas _ [s] = [s]
    1.18 -  | serial_commas conj [s1, s2] = [s1, conj, s2]
    1.19 -  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    1.20 -  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    1.21 -
    1.22  (* int -> string *)
    1.23  fun plural_s n = if n = 1 then "" else "s"
    1.24  (* 'a list -> string *)