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 *)