# HG changeset patch
# User blanchet
# Date 1392222960 -3600
# Node ID ec73f81e49e79088a2cfece238b58a1b12a2c3f0
# Parent  3def821deb70ff21ac1cac8662064e03f3a6942d
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')

diff -r 3def821deb70 -r ec73f81e49e7 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 17:35:59 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 17:36:00 2014 +0100
@@ -1302,7 +1302,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 3def821deb70 -r ec73f81e49e7 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 17:35:59 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 17:36:00 2014 +0100
@@ -178,7 +178,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_inductss co_iter_thmsss disc_co_itersss
diff -r 3def821deb70 -r ec73f81e49e7 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 17:35:59 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 17:36:00 2014 +0100
@@ -60,7 +60,7 @@
 
 fun register_n2m_sugar key n2m_sugar =
   Local_Theory.declaration {syntax = false, pervasive = false}
-    (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar)));
+    (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
 
 fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
     unfold_lets_splits (betapply (arg2, arg1))
diff -r 3def821deb70 -r ec73f81e49e7 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Feb 12 17:35:59 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Feb 12 17:36:00 2014 +0100
@@ -221,9 +221,8 @@
     val constr_keys = map (fst o dest_Const) constrs;
     val data = (case_comb, constrs);
     val Tname = Tname_of_data data;
-    val update_constrs =
-      fold (fn key => Symtab.insert_list (eq_fst (op =)) (key, (Tname, data))) constr_keys;
-    val update_cases = Symtab.default (case_key, data);
+    val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys;
+    val update_cases = Symtab.update (case_key, data);
   in
     context
     |> map_constrs update_constrs
diff -r 3def821deb70 -r ec73f81e49e7 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 17:35:59 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 17:36:00 2014 +0100
@@ -39,7 +39,7 @@
   val ctr_sugars_of: Proof.context -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
   val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
-  val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
+  val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
 
   val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
   val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
@@ -146,9 +146,9 @@
 
 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 =
+fun default_register_ctr_sugar_global key ctr_sugar =
   Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
 
 val isN = "is_";
diff -r 3def821deb70 -r ec73f81e49e7 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Feb 12 17:35:59 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Feb 12 17:36:00 2014 +0100
@@ -130,7 +130,8 @@
           map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
      cases = cases |> fold Symtab.update
        (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
-  fold (fn (key, info) => Ctr_Sugar.register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
+  fold (fn (key, info) =>
+    Ctr_Sugar.default_register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
 
 
 (* complex queries *)