# HG changeset patch
# User haftmann
# Date 1169713954 -3600
# Node ID d9e3e4c30d6bcb97640bcca52e5c723bea8cc909
# Parent  f2bf6bcd4a989747c970cddfafaac65cfb382e57
adjusted names

diff -r f2bf6bcd4a98 -r d9e3e4c30d6b doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Wed Jan 24 20:54:21 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Jan 25 09:32:34 2007 +0100
@@ -1062,7 +1062,7 @@
 
   For technical reasons, we further have to provide a
   synonym for @{const None} which in code generator view
-  is a function rather than a datatype constructor:
+  is a function rather than a term constructor:
 *}
 
 definition
diff -r f2bf6bcd4a98 -r d9e3e4c30d6b src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Jan 24 20:54:21 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Jan 25 09:32:34 2007 +0100
@@ -552,7 +552,7 @@
         val tycos = map fst tycos';
         val tycos'' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
         val _ = if gen_subset (op =) (tycos, tycos'') then () else
-          error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
+          error ("type constructors are not mutually recursive: " ^ (commas o map quote) tycos);
         val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
       in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;