--- a/src/Tools/code/code_target.ML Thu Aug 16 11:45:06 2007 +0200
+++ b/src/Tools/code/code_target.ML Thu Aug 16 11:45:07 2007 +0200
@@ -686,11 +686,12 @@
| fillup_parm x (i, NONE) = x ^ string_of_int i;
fun fish_parms vars eqs =
let
- val raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
- val x = Name.variant (map_filter I raw_fished) "x";
- val fished = map_index (fillup_parm x) raw_fished;
- val vars' = CodeName.intro_vars fished vars;
- in map (CodeName.lookup_var vars') fished end;
+ val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
+ val x = Name.variant (map_filter I fished1) "x";
+ val fished2 = map_index (fillup_parm x) fished1;
+ val (fished3, _) = Name.variants fished2 Name.context;
+ val vars' = CodeName.intro_vars fished3 vars;
+ in map (CodeName.lookup_var vars') fished3 end;
fun pr_eq (ts, t) =
let
val consts = map_filter