--- a/src/Pure/General/same.ML Thu Jul 16 22:22:03 2009 +0200
+++ b/src/Pure/General/same.ML Thu Jul 16 22:54:39 2009 +0200
@@ -10,6 +10,7 @@
exception SAME
type ('a, 'b) function = 'a -> 'b (*exception SAME*)
type 'a operation = ('a, 'a) function (*exception SAME*)
+ val same: ('a, 'b) function
val commit: 'a operation -> 'a -> 'a
val function: ('a -> 'b option) -> ('a, 'b) function
val capture: ('a, 'b) function -> 'a -> 'b option
@@ -25,6 +26,7 @@
type ('a, 'b) function = 'a -> 'b;
type 'a operation = ('a, 'a) function;
+fun same _ = raise SAME;
fun commit f x = f x handle SAME => x;
fun capture f x = SOME (f x) handle SAME => NONE;