# HG changeset patch # User blanchet # Date 1376256959 -7200 # Node ID 717a23e1458640f96dff136029948cdb482b60bb # Parent 1b62f05ab4fd1c76a9838835de4e1f68a9e37de6 avoid DUP exception in local context (cf. 062aa11e98e1) diff -r 1b62f05ab4fd -r 717a23e14586 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Sun Aug 11 23:35:57 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Sun Aug 11 23:35:59 2013 +0200 @@ -1263,7 +1263,7 @@ fun register_bnf key (bnf, lthy) = (bnf, Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy); + (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy); (* TODO: Once the invariant "nwits > 0" holds, remove "mk_conjunction_balanced'" and "rtac TrueI" below *)