prefer new-style Name.invents;
authorwenzelm
Thu Jun 09 15:38:49 2011 +0200 (2011-06-09)
changeset 4332328e71a685c84
parent 43322 1f6f6454f115
child 43324 2b47822868e4
prefer new-style Name.invents;
src/HOL/Tools/Function/fun.ML
src/Pure/Syntax/syntax_ext.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Thu Jun 09 15:37:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Thu Jun 09 15:38:49 2011 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4          val (argTs, rT) = chop n (binder_types fT)
     1.5            |> apsnd (fn Ts => Ts ---> body_type fT)
     1.6  
     1.7 -        val qs = map Free (Name.invent_list [] "a" n ~~ argTs)
     1.8 +        val qs = map Free (Name.invents Name.context "a" n ~~ argTs)
     1.9        in
    1.10          HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
    1.11            Const ("HOL.undefined", rT))
     2.1 --- a/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 15:37:37 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 15:38:49 2011 +0200
     2.3 @@ -241,7 +241,7 @@
     2.4            val rangeT = Term.range_type typ handle Match =>
     2.5              err_in_mfix "Missing structure argument for indexed syntax" mfix;
     2.6  
     2.7 -          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
     2.8 +          val xs = map Ast.Variable (Name.invents Name.context "xa" (length args - 1));
     2.9            val (xs1, xs2) = chop (find_index is_index args) xs;
    2.10            val i = Ast.Variable "i";
    2.11            val lhs = Ast.mk_appl (Ast.Constant indexed_const)
     3.1 --- a/src/Tools/nbe.ML	Thu Jun 09 15:37:37 2011 +0200
     3.2 +++ b/src/Tools/nbe.ML	Thu Jun 09 15:38:49 2011 +0200
     3.3 @@ -372,7 +372,7 @@
     3.4      fun assemble_eqns (c, (num_args, (dicts, eqns))) =
     3.5        let
     3.6          val default_args = map nbe_default
     3.7 -          (Name.invent_list [] "a" (num_args - length dicts));
     3.8 +          (Name.invents Name.context "a" (num_args - length dicts));
     3.9          val eqns' = map_index (assemble_eqn c dicts default_args) eqns
    3.10            @ (if c = "" then [] else [(nbe_fun (length eqns) c,
    3.11              [([ml_list (rev (dicts @ default_args))],
    3.12 @@ -421,7 +421,7 @@
    3.13    | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
    3.14        let
    3.15          val names = map snd super_classes @ map fst classparams;
    3.16 -        val params = Name.invent_list [] "d" (length names);
    3.17 +        val params = Name.invents Name.context "d" (length names);
    3.18          fun mk (k, name) =
    3.19            (name, ([(v, [])],
    3.20              [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],