src/Tools/nbe.ML
changeset 43329 84472e198515
parent 43323 28e71a685c84
child 43619 3803869014aa
     1.1 --- a/src/Tools/nbe.ML	Wed Jun 08 22:16:21 2011 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Jun 09 20:22:22 2011 +0200
     1.3 @@ -330,7 +330,8 @@
     1.4          val vs = (fold o Code_Thingol.fold_varnames)
     1.5            (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args [];
     1.6          val names = Name.make_context (map fst vs);
     1.7 -        fun declare v k ctxt = let val vs = Name.invents ctxt v k
     1.8 +        fun declare v k ctxt =
     1.9 +          let val vs = Name.invent ctxt v k
    1.10            in (vs, fold Name.declare vs ctxt) end;
    1.11          val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
    1.12            then declare v (k - 1) #>> (fn vs => (v, vs))
    1.13 @@ -372,7 +373,7 @@
    1.14      fun assemble_eqns (c, (num_args, (dicts, eqns))) =
    1.15        let
    1.16          val default_args = map nbe_default
    1.17 -          (Name.invents Name.context "a" (num_args - length dicts));
    1.18 +          (Name.invent Name.context "a" (num_args - length dicts));
    1.19          val eqns' = map_index (assemble_eqn c dicts default_args) eqns
    1.20            @ (if c = "" then [] else [(nbe_fun (length eqns) c,
    1.21              [([ml_list (rev (dicts @ default_args))],
    1.22 @@ -421,7 +422,7 @@
    1.23    | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
    1.24        let
    1.25          val names = map snd super_classes @ map fst classparams;
    1.26 -        val params = Name.invents Name.context "d" (length names);
    1.27 +        val params = Name.invent Name.context "d" (length names);
    1.28          fun mk (k, name) =
    1.29            (name, ([(v, [])],
    1.30              [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],