src/Tools/nbe.ML
changeset 43323 28e71a685c84
parent 42405 13ecdb3057d8
child 43329 84472e198515
     1.1 --- a/src/Tools/nbe.ML	Thu Jun 09 15:37:37 2011 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Jun 09 15:38:49 2011 +0200
     1.3 @@ -372,7 +372,7 @@
     1.4      fun assemble_eqns (c, (num_args, (dicts, eqns))) =
     1.5        let
     1.6          val default_args = map nbe_default
     1.7 -          (Name.invent_list [] "a" (num_args - length dicts));
     1.8 +          (Name.invents Name.context "a" (num_args - length dicts));
     1.9          val eqns' = map_index (assemble_eqn c dicts default_args) eqns
    1.10            @ (if c = "" then [] else [(nbe_fun (length eqns) c,
    1.11              [([ml_list (rev (dicts @ default_args))],
    1.12 @@ -421,7 +421,7 @@
    1.13    | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
    1.14        let
    1.15          val names = map snd super_classes @ map fst classparams;
    1.16 -        val params = Name.invent_list [] "d" (length names);
    1.17 +        val params = Name.invents Name.context "d" (length names);
    1.18          fun mk (k, name) =
    1.19            (name, ([(v, [])],
    1.20              [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],