# HG changeset patch # User berghofe # Date 1011620618 -3600 # Node ID 073116d65bb9672ae7f88a67088572b2714a76d4 # Parent ed702a3af45c3c8163c0f0bc49cf4741c22b0f73 datatype_codegen now checks type of constructor. diff -r ed702a3af45c -r 073116d65bb9 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Mon Jan 21 13:44:16 2002 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Mon Jan 21 14:43:38 2002 +0100 @@ -145,12 +145,13 @@ | Some (tname, {index, descr, ...}) => if is_some (get_assoc_code thy s T) then None else let val Some (_, _, constrs) = assoc (descr, index) - in (case assoc (constrs, s) of - None => Some (pretty_case thy gr dep brack + in (case (assoc (constrs, s), strip_type T) of + (None, _) => Some (pretty_case thy gr dep brack (#3 (the (assoc (descr, index)))) c ts) - | Some args => Some (pretty_constr thy + | (Some args, (_, Type _)) => Some (pretty_constr thy (fst (invoke_tycodegen thy dep false (gr, snd (strip_type T)))) - dep brack args c ts)) + dep brack args c ts) + | _ => None) end) | _ => None);