diff -r fc660ec56599 -r 952b81b0572c src/Pure/more_pattern.ML
--- a/src/Pure/more_pattern.ML	Wed Oct 23 14:05:31 2024 +0200
+++ b/src/Pure/more_pattern.ML	Wed Oct 23 14:59:06 2024 +0200
@@ -67,47 +67,41 @@
             NONE => Option.map (rpair skel0) (get_first (fn proc => proc tm) procs)
           | some => some);
 
-    fun rew_sub r bounds _ (Abs (_, _, body) $ t) =
+    fun rew_sub rw bounds _ (Abs (_, _, body) $ t) =
           let val t' = subst_bound (t, body)
-          in SOME (the_default t' (rew_sub r bounds skel0 t')) end
-      | rew_sub r bounds skel (t1 $ t2) =
-          (case r bounds (skel_fun skel) t1 of
-            SOME t1' =>
-              (case r bounds (skel_arg skel) t2 of
-                SOME t2' => SOME (t1' $ t2')
-              | NONE => SOME (t1' $ t2))
-          | NONE =>
-              (case r bounds (skel_arg skel) t2 of
-                SOME t2' => SOME (t1 $ t2')
-              | NONE => NONE))
-      | rew_sub r bounds skel (tm as Abs (x, _, _)) =
-          let val (abs, tm') = variant_absfree bounds x tm in
-            (case r (bounds + 1) (skel_body skel) tm' of
-              SOME tm'' => SOME (abs tm'')
-            | NONE => NONE)
-          end
+          in SOME (the_default t' (rew_sub rw bounds skel0 t')) end
+      | rew_sub rw bounds skel (t $ u) =
+          (case (rw bounds (skel_fun skel) t, rw bounds (skel_arg skel) u) of
+            (SOME t', SOME u') => SOME (t' $ u')
+          | (SOME t', NONE) => SOME (t' $ u)
+          | (NONE, SOME u') => SOME (t $ u')
+          | (NONE, NONE) => NONE)
+      | rew_sub rw bounds skel (t as Abs (x, _, _)) =
+          let val (abs, t') = variant_absfree bounds x t
+          in Option.map abs (rw (bounds + 1) (skel_body skel) t') end
       | rew_sub _ _ _ _ = NONE;
 
     fun rew_bot _ (Var _) _ = NONE
-      | rew_bot bounds skel tm =
-          (case rew_sub rew_bot bounds skel tm of
-            SOME tm1 =>
-              (case rew tm1 of
-                SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
-              | NONE => SOME tm1)
-          | NONE => (case rew tm of
-                SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
+      | rew_bot bounds skel t =
+          (case rew_sub rew_bot bounds skel t of
+            SOME t1 =>
+              (case rew t1 of
+                SOME (t2, skel') => SOME (the_default t2 (rew_bot bounds skel' t2))
+              | NONE => SOME t1)
+          | NONE =>
+              (case rew t of
+                SOME (t1, skel') => SOME (the_default t1 (rew_bot bounds skel' t1))
               | NONE => NONE));
 
-    fun rew_top bounds _ tm =
-      (case rew tm of
-        SOME (tm1, _) =>
-          (case rew_sub rew_top bounds skel0 tm1 of
-            SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
-          | NONE => SOME tm1)
+    fun rew_top bounds _ t =
+      (case rew t of
+        SOME (t1, _) =>
+          (case rew_sub rew_top bounds skel0 t1 of
+            SOME t2 => SOME (the_default t2 (rew_top bounds skel0 t2))
+          | NONE => SOME t1)
       | NONE =>
-          (case rew_sub rew_top bounds skel0 tm of
-            SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
+          (case rew_sub rew_top bounds skel0 t of
+            SOME t1 => SOME (the_default t1 (rew_top bounds skel0 t1))
           | NONE => NONE));
 
   in the_default term ((if bot then rew_bot else rew_top) 0 skel0 term) end;