# HG changeset patch
# User krauss
# Date 1180790792 -7200
# Node ID 98736a2fec98d5c99b9135e2500d104e2ed4b012
# Parent  85612df29daa0822a6ea14f419a60d231588e3a4
added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction

diff -r 85612df29daa -r 98736a2fec98 src/Pure/library.ML
--- 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 =