1.1 --- a/src/Pure/library.scala	Fri May 21 11:16:01 2010 +0200
     1.2 +++ b/src/Pure/library.scala	Fri May 21 11:50:19 2010 +0200
     1.3 @@ -17,6 +17,14 @@
     1.4  
     1.5  object Library
     1.6  {
     1.7 +  /* partial functions */
     1.8 +
     1.9 +  def undefined[A, B] = new PartialFunction[A, B] {
    1.10 +    def apply(x: A): B = throw new NoSuchElementException("undefined")
    1.11 +    def isDefinedAt(x: A) = false
    1.12 +  }
    1.13 +
    1.14 +
    1.15    /* separate */
    1.16  
    1.17    def separate[A](s: A, list: List[A]): List[A] =