# 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 *)