--- a/src/Tools/Code/code_printer.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Jun 09 16:34:49 2011 +0200
@@ -184,7 +184,7 @@
fun fillup_param _ (_, SOME v) = v
| fillup_param x (i, NONE) = x ^ string_of_int i;
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
- val x = Name.variant (map_filter I fished1) "x";
+ val x = singleton (Name.variant_list (map_filter I fished1)) "x";
val fished2 = map_index (fillup_param x) fished1;
val (fished3, _) = Name.variants fished2 Name.context;
val vars' = intro_vars fished3 vars;