tuned -- eliminate clones;

--- a/src/Pure/proofterm.ML	Fri Dec 08 14:35:24 2023 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 08 14:48:17 2023 +0100
@@ -796,27 +796,21 @@
 (* substitution of bound variables *)
 
 fun subst_bounds args prf =
-  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 Term.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;
+  if null args then prf
+  else
+    let
+      val term = Term.subst_bounds_same args;
 
-    fun proof lev (AbsP (a, t, p)) =
-        (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
-          handle Same.SAME => AbsP (a, t, proof lev p))
-      | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
-      | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
-          handle Same.SAME => p %% proof lev q)
-      | proof lev (p % t) = (proof lev p % Option.map (Same.commit (term lev)) t
-          handle Same.SAME => p % Same.map_option (term lev) t)
-      | proof _ _ = raise Same.SAME;
-  in if null args then prf else Same.commit (proof 0) prf end;
+      fun proof lev (AbsP (a, t, p)) =
+          (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
+            handle Same.SAME => AbsP (a, t, proof lev p))
+        | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
+        | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
+            handle Same.SAME => p %% proof lev q)
+        | proof lev (p % t) = (proof lev p % Option.map (Same.commit (term lev)) t
+            handle Same.SAME => p % Same.map_option (term lev) t)
+        | proof _ _ = raise Same.SAME;
+    in Same.commit (proof 0) prf end;
 
 fun subst_pbounds args prf =
   let

--- 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 =