# HG changeset patch
# User wenzelm
# Date 1247777679 -7200
# Node ID e8fbfa84c23f76400c384a411e87b1a6698776bd
# Parent  a5e7c8e60c859eb18678a2917511ec063fd77fc9
added same;

diff -r a5e7c8e60c85 -r e8fbfa84c23f src/Pure/General/same.ML
--- 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;