src/Pure/General/same.ML
changeset 32025 e8fbfa84c23f
parent 32022 c2f4ee07647f
     1.1 --- a/src/Pure/General/same.ML	Thu Jul 16 22:22:03 2009 +0200
     1.2 +++ b/src/Pure/General/same.ML	Thu Jul 16 22:54:39 2009 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    exception SAME
     1.5    type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
     1.6    type 'a operation = ('a, 'a) function  (*exception SAME*)
     1.7 +  val same: ('a, 'b) function
     1.8    val commit: 'a operation -> 'a -> 'a
     1.9    val function: ('a -> 'b option) -> ('a, 'b) function
    1.10    val capture: ('a, 'b) function -> 'a -> 'b option
    1.11 @@ -25,6 +26,7 @@
    1.12  type ('a, 'b) function = 'a -> 'b;
    1.13  type 'a operation = ('a, 'a) function;
    1.14  
    1.15 +fun same _ = raise SAME;
    1.16  fun commit f x = f x handle SAME => x;
    1.17  
    1.18  fun capture f x = SOME (f x) handle SAME => NONE;