--- 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);