src/Tools/code/code_target.ML
changeset 24294 edfe16773fd4
parent 24284 f5afd33f5d02
child 24381 560e8ecdf633
     1.1 --- a/src/Tools/code/code_target.ML	Thu Aug 16 11:45:06 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Thu Aug 16 11:45:07 2007 +0200
     1.3 @@ -686,11 +686,12 @@
     1.4                | fillup_parm x (i, NONE) = x ^ string_of_int i;
     1.5              fun fish_parms vars eqs =
     1.6                let
     1.7 -                val raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
     1.8 -                val x = Name.variant (map_filter I raw_fished) "x";
     1.9 -                val fished = map_index (fillup_parm x) raw_fished;
    1.10 -                val vars' = CodeName.intro_vars fished vars;
    1.11 -              in map (CodeName.lookup_var vars') fished end;
    1.12 +                val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
    1.13 +                val x = Name.variant (map_filter I fished1) "x";
    1.14 +                val fished2 = map_index (fillup_parm x) fished1;
    1.15 +                val (fished3, _) = Name.variants fished2 Name.context;
    1.16 +                val vars' = CodeName.intro_vars fished3 vars;
    1.17 +              in map (CodeName.lookup_var vars') fished3 end;
    1.18              fun pr_eq (ts, t) =
    1.19                let
    1.20                  val consts = map_filter