# HG changeset patch
# User blanchet
# Date 1375194159 -7200
# Node ID 062aa11e98e1a777830155015d4477dbffa441b7
# Parent  3e651be14fcd7415ade06e4217209b95f221b017
avoid DUP error in local context

diff -r 3e651be14fcd -r 062aa11e98e1 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Jul 30 16:22:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Jul 30 16:22:39 2013 +0200
@@ -135,7 +135,7 @@
 
 fun register_fp_sugar key fp_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
-    (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
+    (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss
     co_inducts co_iter_thmsss lthy =