# HG changeset patch
# User wenzelm
# Date 1702298402 -3600
# Node ID 0e15387c03005e52311de62c56257a82fe797baa
# Parent  b0774e7d19496aa65f5e1c93b02deefc32c2f6d9
tuned: more standard accumulation;

diff -r b0774e7d1949 -r 0e15387c0300 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Dec 11 13:03:10 2023 +0100
+++ b/src/Pure/term.ML	Mon Dec 11 13:40:02 2023 +0100
@@ -646,16 +646,14 @@
 
 fun incr_boundvars inc = incr_bv inc 0;
 
-(*Scan a pair of terms; while they are similar,
-  accumulate corresponding bound vars in "al"*)
-fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
-      match_bvs(s, t, if x="" orelse y="" then al
-                                          else (x,y)::al)
-  | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
-  | match_bvs(_,_,al) = al;
+(*Scan a pair of terms; while they are similar, accumulate corresponding bound vars*)
+fun match_bvs (Abs (x, _, s), Abs (y, _, t)) =
+      (x <> "" andalso y <> "") ? cons (x, y) #> match_bvs (s, t)
+  | match_bvs (f $ s, g $ t) = match_bvs (s, t) #> match_bvs (f, g)
+  | match_bvs _ = I;
 
 (* strip abstractions created by parameters *)
-fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al);
+val match_bvars = apply2 strip_abs_body #> match_bvs;
 
 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
@@ -663,7 +661,7 @@
 
 fun rename_abs pat obj t =
   let
-    val ren = match_bvs (pat, obj, []);
+    val ren = match_bvs (pat, obj) [];
     fun ren_abs (Abs (x, T, b)) =
           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
       | ren_abs (f $ t) = ren_abs f $ ren_abs t