--- a/src/Pure/General/same.ML Tue Dec 05 16:38:16 2023 +0100
+++ b/src/Pure/General/same.ML Tue Dec 05 16:39:31 2023 +0100
@@ -13,6 +13,7 @@
val same: ('a, 'b) function
val commit: 'a operation -> 'a -> 'a
val commit_id: 'a operation -> 'a -> 'a * bool
+ val catch: ('a, 'b) function -> 'a -> 'b option
val function: ('a -> 'b option) -> ('a, 'b) function
val map: 'a operation -> 'a list operation
val map_option: ('a, 'b) function -> ('a option, 'b option) function
@@ -30,6 +31,8 @@
fun commit f x = f x handle SAME => x;
fun commit_id f x = (f x, false) handle SAME => (x, true);
+fun catch f x = SOME (f x) handle SAME => NONE;
+
fun function f x =
(case f x of
NONE => raise SAME