diff -r 51868d951a42 -r b83953ac9494 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Thu Dec 07 15:25:29 2023 +0100
+++ b/src/Pure/envir.ML	Thu Dec 07 15:56:54 2023 +0100
@@ -214,13 +214,13 @@
   if Vartab.is_empty tyenv then raise Same.SAME
   else Same.map (norm_type0 tyenv) Ts;
 
-fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
+fun norm_type tyenv = Same.commit (norm_type_same tyenv);
 
 fun norm_term_same (envir as Envir {tenv, tyenv, ...}) =
   if Vartab.is_empty tyenv then norm_term1 tenv
   else norm_term2 envir;
 
-fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
+fun norm_term envir = Same.commit (norm_term_same envir);
 
 fun beta_norm t =
   if Term.could_beta_contract t then norm_term init t else t;
@@ -268,30 +268,33 @@
 
 local
 
-fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
-  | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
-  | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
-  | decr _ _ = raise Same.SAME
-and decrh lev t = (decr lev t handle Same.SAME => t);
+fun decr_same lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
+  | decr_same lev (Abs (a, T, body)) = Abs (a, T, decr_same (lev + 1) body)
+  | decr_same lev (t $ u) =
+      (decr_same lev t $ Same.commit (decr_same lev) u
+        handle Same.SAME => t $ decr_same lev u)
+  | decr_same _ _ = raise Same.SAME;
 
-fun eta (Abs (a, T, body)) =
-    ((case eta body of
+fun eta_same (Abs (a, T, body)) =
+    ((case eta_same body of
         body' as (f $ Bound 0) =>
           if Term.is_dependent f then Abs (a, T, body')
-          else decrh 0 f
+          else Same.commit (decr_same 0) f
      | body' => Abs (a, T, body')) handle Same.SAME =>
         (case body of
           f $ Bound 0 =>
             if Term.is_dependent f then raise Same.SAME
-            else decrh 0 f
+            else Same.commit (decr_same 0) f
         | _ => raise Same.SAME))
-  | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u)
-  | eta _ = raise Same.SAME;
+  | eta_same (t $ u) =
+      (eta_same t $ Same.commit eta_same u
+        handle Same.SAME => t $ eta_same u)
+  | eta_same _ = raise Same.SAME;
 
 in
 
 fun eta_contract t =
-  if Term.could_eta_contract t then Same.commit eta t else t;
+  if Term.could_eta_contract t then Same.commit eta_same t else t;
 
 end;
 
@@ -366,7 +369,9 @@
       | subst (Abs (a, T, t)) =
           (Abs (a, substT T, Same.commit subst t)
             handle Same.SAME => Abs (a, T, subst t))
-      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+      | subst (t $ u) =
+          (subst t $ Same.commit subst u
+            handle Same.SAME => t $ subst u);
   in subst end;
 
 in
@@ -384,9 +389,9 @@
   else if Vartab.is_empty tyenv then subst_term1 tenv
   else subst_term2 tenv tyenv;
 
-fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
-fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
-fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
+fun subst_type tyenv = Same.commit (subst_type_same tyenv);
+fun subst_term_types tyenv = Same.commit (subst_term_types_same tyenv);
+fun subst_term envs = Same.commit (subst_term_same envs);
 
 end;