diff -r 7e67b9706211 -r edfe16773fd4 src/Tools/code/code_target.ML
--- 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