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;