datatype_codegen now checks name of result type of constructor
authorberghofe
Sun Oct 19 21:14:53 2008 +0200 (2008-10-19)
changeset 286399788fb18a142
parent 28638 809dda85079d
child 28640 188e9557c572
datatype_codegen now checks name of result type of constructor
to avoid problems with overloaded constants such as 0.
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Sun Oct 19 20:09:37 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Sun Oct 19 21:14:53 2008 +0200
     1.3 @@ -278,12 +278,14 @@
     1.4            SOME (pretty_case thy defs dep module brack
     1.5              (#3 (the (AList.lookup op = descr index))) c ts gr )
     1.6        | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
     1.7 -        (SOME {index, descr, ...}, (_, U as Type _)) =>
     1.8 +        (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
     1.9            if is_some (get_assoc_code thy (s, T)) then NONE else
    1.10 -          let val SOME args = AList.lookup op =
    1.11 -            (#3 (the (AList.lookup op = descr index))) s
    1.12 +          let
    1.13 +            val SOME (tyname', _, constrs) = AList.lookup op = descr index;
    1.14 +            val SOME args = AList.lookup op = constrs s
    1.15            in
    1.16 -            SOME (pretty_constr thy defs
    1.17 +            if tyname <> tyname' then NONE
    1.18 +            else SOME (pretty_constr thy defs
    1.19                dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
    1.20            end
    1.21        | _ => NONE)