# HG changeset patch
# User wenzelm
# Date 1721559813 -7200
# Node ID 7aa14d4567fe9ad0a36aa4b3e601ddd27193641a
# Parent  4e8845bbcd814003e3c436b85c0269e5a656404e
more operations;

diff -r 4e8845bbcd81 -r 7aa14d4567fe src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Sun Jul 21 12:37:37 2024 +0200
+++ b/src/Pure/General/same.ML	Sun Jul 21 13:03:33 2024 +0200
@@ -12,6 +12,7 @@
   type 'a operation = ('a, 'a) function  (*exception SAME*)
   val same: ('a, 'b) function
   val commit: 'a operation -> 'a -> 'a
+  val commit_if: bool -> 'a operation -> 'a -> 'a
   val commit_id: 'a operation -> 'a -> 'a * bool
   val catch: ('a, 'b) function -> 'a -> 'b option
   val compose: 'a operation -> 'a operation -> 'a operation
@@ -31,6 +32,7 @@
 
 fun same _ = raise SAME;
 fun commit f x = f x handle SAME => x;
+fun commit_if b f x = if b then commit f x else f x;
 fun commit_id f x = (f x, false) handle SAME => (x, true);
 
 fun catch f x = SOME (f x) handle SAME => NONE;