src/HOL/Tools/datatype_codegen.ML
changeset 20071 8f3e1ddb50e6
parent 19886 6bec6daac280
child 20105 454f4be984b7
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:52 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:54 2006 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4            | pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
     1.5                let
     1.6                  val j = length cargs;
     1.7 -                val xs = variantlist (replicate j "x", names);
     1.8 +                val xs = Name.variant_list names (replicate j "x");
     1.9                  val Us' = Library.take (j, fst (strip_type U));
    1.10                  val frees = map Free (xs ~~ Us');
    1.11                  val (gr0, cp) = invoke_codegen thy defs dep module false