1.1 --- a/src/Pure/library.ML	Sat Jun 02 13:52:07 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Sat Jun 02 15:26:32 2007 +0200
     1.3 @@ -159,6 +159,7 @@
     1.4    val suffix: string -> string -> string
     1.5    val unprefix: string -> string -> string
     1.6    val unsuffix: string -> string -> string
     1.7 +  val plural: 'a -> 'a -> 'b list -> 'a
     1.8    val replicate_string: int -> string -> string
     1.9    val translate_string: (string -> string) -> string -> string
    1.10  
    1.11 @@ -796,6 +797,10 @@
    1.12    if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
    1.13    else raise Fail "unsuffix";
    1.14  
    1.15 +(* Ex: "The variable" ^ plural " is" "s are" vs *)
    1.16 +fun plural sg pl [x] = sg
    1.17 +  | plural sg pl _ = pl
    1.18 +
    1.19  fun replicate_string 0 _ = ""
    1.20    | replicate_string 1 a = a
    1.21    | replicate_string k a =