# HG changeset patch
# User wenzelm
# Date 1702845794 -3600
# Node ID d1e5f6d1ddca128b08c0e3ccbc96307bb1fa14cb
# Parent  899f37f6d2183070ae04b0eb2b0b7317d307635c
clarified signature;

diff -r 899f37f6d218 -r d1e5f6d1ddca src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Dec 17 21:34:44 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 17 21:43:14 2023 +0100
@@ -2395,7 +2395,7 @@
           (case rename_bvars dpairs tpairs B As0 of
             SOME {zterm, term} =>
               let
-                fun zproof p = Same.commit (ZTerm.map_proof_same Same.same zterm) p;
+                fun zproof p = ZTerm.map_proof Same.same zterm p;
                 fun proof p = Same.commit (Proofterm.map_proof_terms_same term I) p;
               in (map (strip_apply (Same.commit term) B) As0, deriv_rule1 zproof proof rder) end
           | NONE => (As0, rder))
diff -r 899f37f6d218 -r d1e5f6d1ddca src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sun Dec 17 21:34:44 2023 +0100
+++ b/src/Pure/zterm.ML	Sun Dec 17 21:43:14 2023 +0100
@@ -236,8 +236,8 @@
   val incr_bv_same: int -> int -> zterm Same.operation
   val incr_bv: int -> int -> zterm -> zterm
   val incr_boundvars: int -> zterm -> zterm
-  val map_proof_same: ztyp Same.operation -> zterm Same.operation -> zproof Same.operation
-  val map_proof_types_same: ztyp Same.operation -> zproof Same.operation
+  val map_proof: ztyp Same.operation -> zterm Same.operation -> zproof -> zproof
+  val map_proof_types: ztyp Same.operation -> zproof -> zproof
   val ztyp_of: typ -> ztyp
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
   val zterm_of: theory -> term -> zterm
@@ -456,8 +456,8 @@
       | proof (ZClassp (T, c)) = ZClassp (typ T, c);
   in proof end;
 
-fun map_proof_types_same typ =
-  map_proof_same typ (subst_term_same typ Same.same);
+fun map_proof typ term = Same.commit (map_proof_same typ term);
+fun map_proof_types typ = map_proof typ (subst_term_same typ Same.same);
 
 
 (* convert ztyp / zterm vs. regular typ / term *)
@@ -619,7 +619,7 @@
             |> instantiate_term_same inst_typ;
 
           val norm_term = Same.compose beta_norm_same inst_term;
-        in Same.commit (map_proof_same inst_typ norm_term) prf end
+        in map_proof inst_typ norm_term prf end
   end;
 
 fun norm_cache thy =
@@ -884,7 +884,7 @@
       subst_term_same typ (fn ((x, i), T) =>
         if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
         else raise Same.SAME);
-  in Same.commit (map_proof_same typ term) prf end;
+  in map_proof typ term prf end;
 
 fun instantiate_proof thy (Ts, ts) prf =
   let
@@ -893,7 +893,7 @@
     val inst = ZVars.build (ts |> fold (fn ((v, T), t) => ZVars.add ((v, ztyp T), zterm t)));
     val typ = instantiate_type_same instT;
     val term = instantiate_term_same typ inst;
-  in Same.commit (map_proof_same typ term) prf end;
+  in map_proof typ term prf end;
 
 fun varifyT_proof names prf =
   if null names then prf
@@ -905,7 +905,7 @@
           (case ZTVars.lookup tab v of
             NONE => raise Same.SAME
           | SOME w => ZTVar w)));
-    in Same.commit (map_proof_types_same typ) prf end;
+    in map_proof_types typ prf end;
 
 fun legacy_freezeT_proof t prf =
   (case Type.legacy_freezeT t of
@@ -914,7 +914,7 @@
       let
         val tvar = ztyp_of o Same.function f;
         val typ = ZTypes.unsynchronized_cache (subst_type_same tvar);
-      in Same.commit (map_proof_types_same typ) prf end);
+      in map_proof_types typ prf end);
 
 
 (* permutations *)
@@ -954,7 +954,7 @@
     val typ = incr_tvar_same inc;
     fun var ((x, i), T) = if i >= 0 then ZVar ((x, i + inc), T) else raise Same.SAME;
     val term = subst_term_same typ var;
-  in Same.commit (map_proof_same typ term) prf end;
+  in map_proof typ term prf end;
 
 fun lift_proof thy gprop inc prems prf =
   let