added undefined: 'a -> 'b;
authorwenzelm
Thu, 19 Jul 2007 23:18:43 +0200
changeset 23860 31f5c9e43e57
parent 23859 fc44fa554ca8
child 23861 72bb3494746f
added undefined: 'a -> 'b;
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;