Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
parse translations for cases are conservative wrt. overloaded constructors
authorhaftmann
Wed, 20 May 2009 10:37:37 +0200
changeset 31208 1ef2f0af7f26
parent 31207 7eb05fc49b45
child 31209 77da3aad5917
parse translations for cases are conservative wrt. overloaded constructors
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle