tuned;

--- a/src/Pure/proofterm.ML	Mon Jan 08 22:26:04 2024 +0100
+++ b/src/Pure/proofterm.ML	Mon Jan 08 22:53:38 2024 +0100
@@ -499,21 +499,23 @@
   | compact_proof (p %% q) = atomic_proof q andalso compact_proof p
   | compact_proof p = atomic_proof p;
 
-fun (prf %> t) = prf % SOME t;
+fun (p %> t) = p % SOME t;
 
 val proof_combt = Library.foldl (op %>);
 val proof_combt' = Library.foldl (op %);
 val proof_combP = Library.foldl (op %%);
 
 fun strip_combt prf =
-    let fun stripc (prf % t, ts) = stripc (prf, t::ts)
-          | stripc  x =  x
-    in  stripc (prf, [])  end;
+  let
+    fun strip (p % t, ts) = strip (p, t :: ts)
+      | strip res = res;
+  in strip (prf, []) end;
 
 fun strip_combP prf =
-    let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs)
-          | stripc  x =  x
-    in  stripc (prf, [])  end;
+  let
+    fun strip (p %% q, qs) = strip (p, q :: qs)
+      | strip res = res;
+  in strip (prf, []) end;
 
 fun strip_thm_body (body as PBody {proof, ...}) =
   (case fst (strip_combt (fst (strip_combP proof))) of

--- a/src/Pure/term.ML	Mon Jan 08 22:26:04 2024 +0100
+++ b/src/Pure/term.ML	Mon Jan 08 22:53:38 2024 +0100
@@ -429,19 +429,21 @@
 
 
 (*maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
-fun strip_comb u : term * term list =
-    let fun stripc (f$t, ts) = stripc (f, t::ts)
-        |   stripc  x =  x
-    in  stripc(u,[])  end;
+fun strip_comb tm =
+  let
+    fun strip (f $ t, ts) = strip (f, t :: ts)
+      | strip res = res;
+  in strip (tm, []) end;
 
-fun args_of u =
-    let fun args (f $ x) xs = args f (x :: xs)
-        |   args _ xs = xs
-    in args u [] end;
+val args_of =
+  let
+    fun args (f $ t) ts = args f (t :: ts)
+      | args _ ts = ts;
+  in build o args end;
 
 (*maps   f(t1,...,tn)  to  f , which is never a combination*)
-fun head_of (f$t) = head_of f
-  | head_of u = u;
+fun head_of (f $ _) = head_of f
+  | head_of t = t;
 
 (*number of atoms and abstractions in a term*)
 fun size_of_term tm =