src/Pure/Syntax/ast.ML
changeset 74232 1091880266e5
parent 69575 f77cc54f6d47
child 80809 4a64fc4d1cde
--- a/src/Pure/Syntax/ast.ML	Sat Sep 04 20:01:43 2021 +0200
+++ b/src/Pure/Syntax/ast.ML	Sat Sep 04 21:25:08 2021 +0200
@@ -158,7 +158,7 @@
           end
       | _ => (ast, []));
   in
-    SOME (mtch head pat Symtab.empty, args) handle NO_MATCH => NONE
+    SOME (Symtab.build (mtch head pat), args) handle NO_MATCH => NONE
   end;