--- a/src/Tools/Code/code_printer.ML Sat Nov 30 23:30:36 2024 +0100
+++ b/src/Tools/Code/code_printer.ML Sun Dec 01 14:01:47 2024 +0100
@@ -188,7 +188,7 @@
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
val x = singleton (Name.variant_list (map_filter I fished1)) "x";
val fished2 = map_index (fillup_param x) fished1;
- val (fished3, _) = fold_map Name.variant fished2 Name.context;
+ val fished3 = Name.variants Name.context fished2;
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;