adjusted names
authorhaftmann
Thu Jan 25 09:32:34 2007 +0100 (2007-01-25)
changeset 22175d9e3e4c30d6b
parent 22174 f2bf6bcd4a98
child 22176 29ba33d58637
adjusted names
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed Jan 24 20:54:21 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jan 25 09:32:34 2007 +0100
     1.3 @@ -1062,7 +1062,7 @@
     1.4  
     1.5    For technical reasons, we further have to provide a
     1.6    synonym for @{const None} which in code generator view
     1.7 -  is a function rather than a datatype constructor:
     1.8 +  is a function rather than a term constructor:
     1.9  *}
    1.10  
    1.11  definition
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Jan 24 20:54:21 2007 +0100
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Jan 25 09:32:34 2007 +0100
     2.3 @@ -552,7 +552,7 @@
     2.4          val tycos = map fst tycos';
     2.5          val tycos'' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
     2.6          val _ = if gen_subset (op =) (tycos, tycos'') then () else
     2.7 -          error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
     2.8 +          error ("type constructors are not mutually recursive: " ^ (commas o map quote) tycos);
     2.9          val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
    2.10        in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
    2.11