avoid DUP exception in local context (cf. 062aa11e98e1)
authorblanchet
Sun, 11 Aug 2013 23:35:59 +0200
changeset 52957 717a23e14586
parent 52956 1b62f05ab4fd
child 52958 5a77edcdbe54
avoid DUP exception in local context (cf. 062aa11e98e1)
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 *)