added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction

--- a/src/Pure/library.ML	Sat Jun 02 13:52:07 2007 +0200
+++ b/src/Pure/library.ML	Sat Jun 02 15:26:32 2007 +0200
@@ -159,6 +159,7 @@
   val suffix: string -> string -> string
   val unprefix: string -> string -> string
   val unsuffix: string -> string -> string
+  val plural: 'a -> 'a -> 'b list -> 'a
   val replicate_string: int -> string -> string
   val translate_string: (string -> string) -> string -> string
 
@@ -796,6 +797,10 @@
   if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
   else raise Fail "unsuffix";
 
+(* Ex: "The variable" ^ plural " is" "s are" vs *)
+fun plural sg pl [x] = sg
+  | plural sg pl _ = pl
+
 fun replicate_string 0 _ = ""
   | replicate_string 1 a = a
   | replicate_string k a =