added Library.undefined (in Scala);

--- a/src/Pure/library.scala	Fri May 21 11:16:01 2010 +0200
+++ b/src/Pure/library.scala	Fri May 21 11:50:19 2010 +0200
@@ -17,6 +17,14 @@
 
 object Library
 {
+  /* partial functions */
+
+  def undefined[A, B] = new PartialFunction[A, B] {
+    def apply(x: A): B = throw new NoSuchElementException("undefined")
+    def isDefinedAt(x: A) = false
+  }
+
+
   /* separate */
 
   def separate[A](s: A, list: List[A]): List[A] =