--- a/src/HOL/Tools/function_package/fundef_lib.ML Sat Jun 02 15:26:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Sat Jun 02 15:28:38 2007 +0200
@@ -10,12 +10,6 @@
structure FundefLib = struct
-(* ==> library/string *)
-fun plural sg pl [x] = sg
- | plural sg pl _ = pl
-
-
-
fun map_option f NONE = NONE
| map_option f (SOME x) = SOME (f x);
@@ -25,11 +19,6 @@
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 *)