changeset 75353 | 05f7f5454cb6 |
parent 74231 | b3c65c984210 |
child 75356 | fa014f31f208 |
--- a/src/Tools/Code/code_printer.ML Sun Mar 27 19:27:50 2022 +0000 +++ b/src/Tools/Code/code_printer.ML Sun Mar 27 19:27:52 2022 +0000 @@ -341,7 +341,7 @@ fun gen_print_bind print_term thm (fxy : fixity) pat vars = let - val vs = Code_Thingol.fold_varnames (insert (op =)) pat []; + val vs = build (Code_Thingol.fold_varnames (insert (op =)) pat); val vars' = intro_vars vs vars; in (print_term thm vars' fxy pat, vars') end;