diff -r 1e7b60cb7694 -r cf750881f1fe src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sat Oct 12 14:55:46 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Sat Oct 12 15:00:56 2024 +0200
@@ -152,27 +152,31 @@
 
 (* match *)
 
-local exception NO_MATCH in
+local
+
+exception NO_MATCH;
 
-fun match obj pat =
+fun match1 (Constant a) (Constant b) env = if a = b then env else raise NO_MATCH
+  | match1 (Variable a) (Constant b) env = if a = b then env else raise NO_MATCH
+  | match1 ast (Variable x) env = Symtab.update (x, ast) env
+  | match1 (Appl asts) (Appl pats) env = match2 asts pats env
+  | match1 _ _ _ = raise NO_MATCH
+and match2 (ast :: asts) (pat :: pats) env = match1 ast pat env |> match2 asts pats
+  | match2 [] [] env = env
+  | match2 _ _ _ = raise NO_MATCH;
+
+in
+
+fun match ast pat =
   let
-    fun match1 (Constant a) (Constant b) env = if a = b then env else raise NO_MATCH
-      | match1 (Variable a) (Constant b) env = if a = b then env else raise NO_MATCH
-      | match1 ast (Variable x) env = Symtab.update (x, ast) env
-      | match1 (Appl asts) (Appl pats) env = match2 asts pats env
-      | match1 _ _ _ = raise NO_MATCH
-    and match2 (ast :: asts) (pat :: pats) env = match1 ast pat env |> match2 asts pats
-      | match2 [] [] env = env
-      | match2 _ _ _ = raise NO_MATCH;
-
     val (head, args) =
-      (case (obj, pat) of
+      (case (ast, pat) of
         (Appl asts, Appl pats) =>
           let val a = length asts and p = length pats in
             if a > p then (Appl (take p asts), drop p asts)
-            else (obj, [])
+            else (ast, [])
           end
-      | _ => (obj, []));
+      | _ => (ast, []));
   in SOME (Symtab.build (match1 head pat), args) handle NO_MATCH => NONE end;
 
 end;