# HG changeset patch
# User wenzelm
# Date 1307626729 -7200
# Node ID 28e71a685c84b129ccf4c7482b3d42e49b49d2fc
# Parent  1f6f6454f115da9a637c985bbafbdf29ce591205
prefer new-style Name.invents;

diff -r 1f6f6454f115 -r 28e71a685c84 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Thu Jun 09 15:37:37 2011 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Thu Jun 09 15:38:49 2011 +0200
@@ -64,7 +64,7 @@
         val (argTs, rT) = chop n (binder_types fT)
           |> apsnd (fn Ts => Ts ---> body_type fT)
 
-        val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
+        val qs = map Free (Name.invents Name.context "a" n ~~ argTs)
       in
         HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
           Const ("HOL.undefined", rT))
diff -r 1f6f6454f115 -r 28e71a685c84 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 15:37:37 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 15:38:49 2011 +0200
@@ -241,7 +241,7 @@
           val rangeT = Term.range_type typ handle Match =>
             err_in_mfix "Missing structure argument for indexed syntax" mfix;
 
-          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
+          val xs = map Ast.Variable (Name.invents Name.context "xa" (length args - 1));
           val (xs1, xs2) = chop (find_index is_index args) xs;
           val i = Ast.Variable "i";
           val lhs = Ast.mk_appl (Ast.Constant indexed_const)
diff -r 1f6f6454f115 -r 28e71a685c84 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Jun 09 15:37:37 2011 +0200
+++ b/src/Tools/nbe.ML	Thu Jun 09 15:38:49 2011 +0200
@@ -372,7 +372,7 @@
     fun assemble_eqns (c, (num_args, (dicts, eqns))) =
       let
         val default_args = map nbe_default
-          (Name.invent_list [] "a" (num_args - length dicts));
+          (Name.invents Name.context "a" (num_args - length dicts));
         val eqns' = map_index (assemble_eqn c dicts default_args) eqns
           @ (if c = "" then [] else [(nbe_fun (length eqns) c,
             [([ml_list (rev (dicts @ default_args))],
@@ -421,7 +421,7 @@
   | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
       let
         val names = map snd super_classes @ map fst classparams;
-        val params = Name.invent_list [] "d" (length names);
+        val params = Name.invents Name.context "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
             [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],