# HG changeset patch
# User wenzelm
# Date 1180905404 -7200
# Node ID 49c78d67b807d1ac9a799615c07f34ab7b2335f7
# Parent  20b5558a54198480203c9944e645f6002c6f8ae4
added plural (from Pure/library.ML);
removed unused eq_str;

diff -r 20b5558a5419 -r 49c78d67b807 src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Sun Jun 03 23:16:43 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sun Jun 03 23:16:44 2007 +0200
@@ -6,8 +6,6 @@
 Some fairly general functions that should probably go somewhere else... 
 *)
 
-
-
 structure FundefLib = struct
 
 fun map_option f NONE = NONE 
@@ -19,8 +17,9 @@
 fun fold_map_option f NONE y = (NONE, y)
   | fold_map_option f (SOME x) y = apfst SOME (f x y);
 
-(* ??? *)
-fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
+(* Ex: "The variable" ^ plural " is" "s are" vs *)
+fun plural sg pl [x] = sg
+  | plural sg pl _ = pl
 
 (* ==> logic.ML? *)
 fun mk_forall v t = all (fastype_of v) $ lambda v t