--- a/src/Pure/General/same.ML Mon Sep 25 21:30:46 2023 +0200
+++ b/src/Pure/General/same.ML Mon Sep 25 21:36:46 2023 +0200
@@ -13,7 +13,6 @@
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
val map: 'a operation -> 'a list operation
val map_option: ('a, 'b) function -> ('a option, 'b option) function
end;
@@ -29,8 +28,6 @@
fun same _ = raise SAME;
fun commit f x = f x handle SAME => x;
-fun capture f x = SOME (f x) handle SAME => NONE;
-
fun function f x =
(case f x of
NONE => raise SAME