# HG changeset patch
# User blanchet
# Date 1391702747 -3600
# Node ID a87e49f4336db6623995c245914af74047f2a0db
# Parent  d344d663658a2a50f204175eda7b796a34a85447
allow multiple registration of the same type, the last wins

diff -r d344d663658a -r a87e49f4336d src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Feb 06 13:04:06 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Feb 06 17:05:47 2014 +0100
@@ -1307,7 +1307,7 @@
 
 fun register_bnf key (bnf, lthy) =
   (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
-    (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy);
+    (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) lthy);
 
 fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
   (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
diff -r d344d663658a -r a87e49f4336d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Feb 06 13:04:06 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Feb 06 17:05:47 2014 +0100
@@ -180,7 +180,7 @@
 
 fun register_fp_sugar key fp_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
-    (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
+    (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
     ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
diff -r d344d663658a -r a87e49f4336d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Feb 06 13:04:06 2014 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Feb 06 17:05:47 2014 +0100
@@ -152,10 +152,10 @@
 
 fun register_ctr_sugar key ctr_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
-    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
+    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)));
 
 fun register_ctr_sugar_global key ctr_sugar =
-  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
+  Context.theory_map (Data.map (Symtab.update (key, ctr_sugar)));
 
 val rep_compat_prefix = "new";