src/HOL/Tools/datatype_codegen.ML
changeset 20192 956cd30ef3be
parent 20190 03a8d7c070d3
child 20382 39964c8dcd54
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Jul 25 16:43:47 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jul 25 16:51:26 2006 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4        in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
     1.5      fun mk_cons tyco (c, tys) =
     1.6        let
     1.7 -        val ts = Name.give_names Name.context "a" tys;
     1.8 +        val ts = Name.names Name.context "a" tys;
     1.9          val ty = tys ---> Type (tyco, map TFree vs);
    1.10        in list_comb (Const (c, ty), map Free ts) end;
    1.11    in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
    1.12 @@ -379,7 +379,7 @@
    1.13      | SOME insts => let
    1.14          fun proven ((tyco, asorts), sort) =
    1.15            Sorts.of_sort (Sign.classes_of thy)
    1.16 -            (Type (tyco, map TFree (Name.give_names Name.context "'a" asorts)), sort);
    1.17 +            (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
    1.18          val (arities, css) = (split_list o map_filter
    1.19            (fn (tyco, (arity, cs)) => if proven arity
    1.20              then NONE else SOME (arity, (tyco, cs)))) insts;
    1.21 @@ -395,7 +395,7 @@
    1.22  
    1.23  fun dest_case_app cs ts tys =
    1.24    let
    1.25 -    val abs = Name.give_names Name.context "a" (Library.drop (length ts, tys));
    1.26 +    val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
    1.27      val (ts', t) = split_last (ts @ map Free abs);
    1.28      val (tys', sty) = split_last tys;
    1.29      fun freenames_of t = fold_aterms