src/HOL/Tools/datatype_codegen.ML
changeset 22175 d9e3e4c30d6b
parent 22052 792c18b8f214
child 22296 c9e7c6e73de3
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Jan 24 20:54:21 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Jan 25 09:32:34 2007 +0100
     1.3 @@ -552,7 +552,7 @@
     1.4          val tycos = map fst tycos';
     1.5          val tycos'' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
     1.6          val _ = if gen_subset (op =) (tycos, tycos'') then () else
     1.7 -          error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
     1.8 +          error ("type constructors are not mutually recursive: " ^ (commas o map quote) tycos);
     1.9          val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
    1.10        in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
    1.11