tuned: more standard argument order;

--- a/src/Pure/proofterm.ML	Thu Dec 07 10:06:51 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 07 10:34:57 2023 +0100
@@ -812,23 +812,23 @@
           handle Same.SAME => prf % Same.map_option (subst' lev) t)
       | subst _ _ = raise Same.SAME
     and substh lev prf = (subst lev prf handle Same.SAME => prf);
-  in (case args of [] => prf | _ => substh 0 prf) end;
+  in if null args then prf else substh 0 prf end;
 
 fun prf_subst_pbounds args prf =
   let
     val n = length args;
-    fun subst (PBound i) Plev tlev =
+    fun subst Plev tlev (PBound i) =
          (if i < Plev then raise Same.SAME    (*var is locally bound*)
           else incr_pboundvars Plev tlev (nth args (i-Plev))
                  handle General.Subscript => PBound (i-n)  (*loose: change it*))
-      | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
-      | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
-      | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev
-          handle Same.SAME => prf %% subst prf' Plev tlev)
-      | subst (prf % t) Plev tlev = subst prf Plev tlev % t
+      | subst Plev tlev (AbsP (a, t, body)) = AbsP (a, t, subst (Plev+1) tlev body)
+      | subst Plev tlev (Abst (a, T, body)) = Abst (a, T, subst Plev (tlev+1) body)
+      | subst Plev tlev (prf %% prf') = (subst Plev tlev prf %% substh Plev tlev prf'
+          handle Same.SAME => prf %% subst Plev tlev prf')
+      | subst Plev tlev (prf % t) = subst Plev tlev prf % t
       | subst  _ _ _ = raise Same.SAME
-    and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf)
-  in (case args of [] => prf | _ => substh prf 0 0) end;
+    and substh Plev tlev prf = (subst Plev tlev prf handle Same.SAME => prf)
+  in if null args then prf else substh 0 0 prf end;
 
 
 (* freezing and thawing of variables in proof terms *)

--- a/src/Pure/term.ML	Thu Dec 07 10:06:51 2023 +0100
+++ b/src/Pure/term.ML	Thu Dec 07 10:34:57 2023 +0100
@@ -700,30 +700,30 @@
 fun subst_bounds (args: term list, t) : term =
   let
     val n = length args;
-    fun subst (t as Bound i, lev) =
+    fun subst lev (Bound i) =
          (if i < lev then raise Same.SAME   (*var is locally bound*)
           else incr_boundvars lev (nth args (i - lev))
             handle General.Subscript => Bound (i - n))  (*loose: change it*)
-      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
-      | subst (f $ t, lev) =
-          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
-            handle Same.SAME => f $ subst (t, lev))
-      | subst _ = raise Same.SAME;
-  in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
+      | subst lev (Abs (a, T, body)) = Abs (a, T, subst (lev + 1) body)
+      | subst lev (f $ t) =
+          (subst lev f $ (subst lev t handle Same.SAME => t)
+            handle Same.SAME => f $ subst lev t)
+      | subst _ _ = raise Same.SAME;
+  in if null args then t else (subst 0 t handle Same.SAME => t) end;
 
 (*Special case: one argument*)
 fun subst_bound (arg, t) : term =
   let
-    fun subst (Bound i, lev) =
+    fun subst lev (Bound i) =
           if i < lev then raise Same.SAME   (*var is locally bound*)
           else if i = lev then incr_boundvars lev arg
           else Bound (i - 1)   (*loose: change it*)
-      | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
-      | subst (f $ t, lev) =
-          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
-            handle Same.SAME => f $ subst (t, lev))
-      | subst _ = raise Same.SAME;
-  in subst (t, 0) handle Same.SAME => t end;
+      | subst lev (Abs (a, T, body)) = Abs (a, T, subst (lev + 1) body)
+      | subst lev (f $ t) =
+          (subst lev f $ (subst lev t handle Same.SAME => t)
+            handle Same.SAME => f $ subst lev t)
+      | subst _ _ = raise Same.SAME;
+  in subst 0 t handle Same.SAME => t end;
 
 (*beta-reduce if possible, else form application*)
 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)