avoid DUP exception in local context (cf. 062aa11e98e1)
--- 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 *)