--- 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);
--- a/src/Pure/proofterm.ML Sat Dec 30 22:36:41 2023 +0100
+++ b/src/Pure/proofterm.ML Sat Dec 30 22:53:03 2023 +0100
@@ -558,12 +558,11 @@
fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => PClass (typ T, c));
fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
-fun same eq f x =
- let val x' = f x
- in if eq (x, x') then raise Same.SAME else x' end;
+fun map_proof_terms f g =
+ Same.commit (map_proof_terms_same (Same.function_eq (op =) f) (Same.function_eq (op =) g));
-fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
-fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
+fun map_proof_types f =
+ Same.commit (map_proof_types_same (Same.function_eq (op =) f));
fun fold_proof_terms f (Abst (_, _, prf)) = fold_proof_terms f prf
| fold_proof_terms f (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f prf