# HG changeset patch
# User haftmann
# Date 1242808657 -7200
# Node ID 1ef2f0af7f265a751cbf1832242e0c3a0f9dd9ca
# Parent  7eb05fc49b45596e14fba105eb2e53fb35b3463c
parse translations for cases are conservative wrt. overloaded constructors

diff -r 7eb05fc49b45 -r 1ef2f0af7f26 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed May 20 10:37:37 2009 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed May 20 10:37:37 2009 +0200
@@ -101,7 +101,7 @@
 fun put_dt_infos (dt_infos : (string * datatype_info) list) =
   map_datatypes (fn {types, constrs, cases} =>
     {types = fold Symtab.update dt_infos types,
-     constrs = fold Symtab.update
+     constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
        (maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
           (#3 (the (AList.lookup op = descr index)))) dt_infos) constrs,
      cases = fold Symtab.update