# HG changeset patch
# User wenzelm
# Date 1701790771 -3600
# Node ID cd17a90523d459c3f9746e213c0f98c8e7e6d4eb
# Parent  3ae09d27ee7aea91a721c97249b94d444ecf7705
more operations;

diff -r 3ae09d27ee7a -r cd17a90523d4 src/Pure/General/same.ML
--- 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