diff -r 11b53e039f6f -r 0824ca1f1da0 src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Sat Dec 30 22:36:41 2023 +0100
+++ b/src/Pure/General/same.ML	Sat Dec 30 22:53:03 2023 +0100
@@ -16,6 +16,7 @@
   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 function_eq: ('a * 'b -> bool) -> ('a -> 'b) -> ('a, 'b) function
   val map: 'a operation -> 'a list operation
   val map_option: ('a, 'b) function -> ('a option, 'b option) function
 end;
@@ -44,6 +45,10 @@
     NONE => raise SAME
   | SOME y => y);
 
+fun function_eq eq f x =
+  let val y = f x
+  in if eq (x, y) then raise SAME else y end;
+
 fun map f [] = raise SAME
   | map f (x :: xs) = (f x :: commit (map f) xs handle SAME => x :: map f xs);