--- 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