diff -r 5d27271701a2 -r 626d00cb4d9c src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Dec 08 14:35:24 2023 +0100
+++ b/src/Pure/term.ML	Fri Dec 08 14:48:17 2023 +0100
@@ -90,6 +90,7 @@
   val loose_bnos: term -> int list
   val loose_bvar: term * int -> bool
   val loose_bvar1: term * int -> bool
+  val subst_bounds_same: term list -> int -> term Same.operation
   val subst_bounds: term list * term -> term
   val subst_bound: term * term -> term
   val betapply: term * term -> term
@@ -704,19 +705,24 @@
   Loose bound variables >=n are reduced by "n" to
      compensate for the disappearance of lambdas.
 *)
+fun subst_bounds_same args =
+  if null args then fn _ => Same.same
+  else
+    let
+      val n = length args;
+      fun term lev (Bound i) =
+           (if i < lev then raise Same.SAME   (*var is locally bound*)
+            else if i - lev < n then incr_boundvars lev (nth args (i - lev))
+            else Bound (i - n))  (*loose: change it*)
+        | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
+        | term lev (t $ u) =
+            (term lev t $ Same.commit (term lev) u
+              handle Same.SAME => t $ term lev u)
+        | term _ _ = raise Same.SAME;
+    in term end;
+
 fun subst_bounds (args: term list, body) : term =
-  let
-    val n = length args;
-    fun term lev (Bound i) =
-         (if i < lev then raise Same.SAME   (*var is locally bound*)
-          else if i - lev < n then incr_boundvars lev (nth args (i - lev))
-          else Bound (i - n))  (*loose: change it*)
-      | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
-      | term lev (t $ u) =
-          (term lev t $ Same.commit (term lev) u
-            handle Same.SAME => t $ term lev u)
-      | term _ _ = raise Same.SAME;
-  in if null args then body else Same.commit (term 0) body end;
+  if null args then body else Same.commit (subst_bounds_same args 0) body;
 
 (*Special case: one argument*)
 fun subst_bound (arg, body) : term =