src/Pure/zterm.ML

   val fold_proof_terms: (zterm -> 'a -> 'a) -> zproof -> 'a -> 'a
   val exists_proof_terms: (zterm -> bool) -> zproof -> bool
   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
   val typ_of: ztyp -> typ
   val term_of: theory -> zterm -> term

       | proof (ZAppp (p, q)) =
           (ZAppp (proof p, Same.commit proof q) handle Same.SAME => ZAppp (p, proof q))
       | 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 *)
 
 fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)

           val inst_term =
             ZVars.build (visible |> (fold o Term.fold_aterms) (fn Var v => add_var v | _ => I))
             |> 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 =
   let
     val {ztyp, zterm} = zterm_cache thy;

             else raise Same.SAME));
     val term =
       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
     val {ztyp, zterm} = zterm_cache thy;
     val instT = ZTVars.build (Ts |> fold (fn (v, T) => ZTVars.add (v, ztyp T)));
     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
   else
     let

       val typ =
         ZTypes.unsynchronized_cache (subst_type_same (fn v =>
           (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
     NONE => prf
   | SOME f =>
       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 *)
 
 fun rotate_proof thy Bs Bi' params asms m prf =

 fun incr_indexes_proof inc prf =
   let
     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
     val {ztyp, zterm} = zterm_cache thy;