src/Pure/General/same.ML

   type 'a operation = ('a, 'a) function  (*exception SAME*)
   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 compose: 'a operation -> 'a operation -> 'a operation
   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
 end;
 

 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 compose g f x =
+  (case catch f x of
+    NONE => g x
+  | SOME y => commit g y);
+
 fun function f x =
   (case f x of
     NONE => raise SAME
   | SOME y => y);