# HG changeset patch
# User berghofe
# Date 1224443693 -7200
# Node ID 9788fb18a142a46da3b03dfd87adccf5c1ea1d55
# Parent  809dda85079d36c6925e44eb8c2f86e465fe3d31
datatype_codegen now checks name of result type of constructor
to avoid problems with overloaded constants such as 0.

diff -r 809dda85079d -r 9788fb18a142 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Sun Oct 19 20:09:37 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Sun Oct 19 21:14:53 2008 +0200
@@ -278,12 +278,14 @@
           SOME (pretty_case thy defs dep module brack
             (#3 (the (AList.lookup op = descr index))) c ts gr )
       | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
-        (SOME {index, descr, ...}, (_, U as Type _)) =>
+        (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
-          let val SOME args = AList.lookup op =
-            (#3 (the (AList.lookup op = descr index))) s
+          let
+            val SOME (tyname', _, constrs) = AList.lookup op = descr index;
+            val SOME args = AList.lookup op = constrs s
           in
-            SOME (pretty_constr thy defs
+            if tyname <> tyname' then NONE
+            else SOME (pretty_constr thy defs
               dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
           end
       | _ => NONE)