Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adjusted names
authorhaftmann
Thu, 25 Jan 2007 09:32:34 +0100
changeset 22175 d9e3e4c30d6b
parent 22174 f2bf6bcd4a98
child 22176 29ba33d58637
adjusted names
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/datatype_codegen.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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;
isabelle