src/Tools/Code/code_printer.ML
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;