# HG changeset patch
# User wenzelm
# Date 1703973183 -3600
# Node ID 0824ca1f1da02a42051d893e49451db56a703f68
# Parent  11b53e039f6f6d263403f2dad8b416d773fdc837
clarified modules;

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);
 
diff -r 11b53e039f6f -r 0824ca1f1da0 src/Pure/proofterm.ML
--- 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