# HG changeset patch
# User wenzelm
# Date 1184879923 -7200
# Node ID 31f5c9e43e57cfa743409f089d6ad519f4cb2c77
# Parent  fc44fa554ca83f95aae7e7b471c02a6ffe655519
added undefined: 'a -> 'b;

diff -r fc44fa554ca8 -r 31f5c9e43e57 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jul 19 21:47:46 2007 +0200
+++ b/src/Pure/library.ML	Thu Jul 19 23:18:43 2007 +0200
@@ -19,6 +19,7 @@
 signature BASIC_LIBRARY =
 sig
   (*functions*)
+  val undefined: 'a -> 'b
   val I: 'a -> 'a
   val K: 'a -> 'b -> 'a
   val flip: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
@@ -245,6 +246,8 @@
 
 (* functions *)
 
+fun undefined _ = raise Match;
+
 fun I x = x;
 fun K x = fn _ => x;
 fun flip f x y = f y x;