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')
authorblanchet
Wed Feb 12 17:36:00 2014 +0100 (2014-02-12)
changeset 55444ec73f81e49e7
parent 55443 3def821deb70
child 55445 a76c679c0218
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')
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/Ctr_Sugar/case_translation.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 17:35:59 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 17:36:00 2014 +0100
     1.3 @@ -1302,7 +1302,7 @@
     1.4  
     1.5  fun register_bnf key (bnf, lthy) =
     1.6    (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
     1.7 -    (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy);
     1.8 +    (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) lthy);
     1.9  
    1.10  fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
    1.11    (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 17:35:59 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 17:36:00 2014 +0100
     2.3 @@ -178,7 +178,7 @@
     2.4  
     2.5  fun register_fp_sugar key fp_sugar =
     2.6    Local_Theory.declaration {syntax = false, pervasive = true}
     2.7 -    (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
     2.8 +    (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
     2.9  
    2.10  fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
    2.11      ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 17:35:59 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 17:36:00 2014 +0100
     3.3 @@ -60,7 +60,7 @@
     3.4  
     3.5  fun register_n2m_sugar key n2m_sugar =
     3.6    Local_Theory.declaration {syntax = false, pervasive = false}
     3.7 -    (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar)));
     3.8 +    (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
     3.9  
    3.10  fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
    3.11      unfold_lets_splits (betapply (arg2, arg1))
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Feb 12 17:35:59 2014 +0100
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Feb 12 17:36:00 2014 +0100
     4.3 @@ -221,9 +221,8 @@
     4.4      val constr_keys = map (fst o dest_Const) constrs;
     4.5      val data = (case_comb, constrs);
     4.6      val Tname = Tname_of_data data;
     4.7 -    val update_constrs =
     4.8 -      fold (fn key => Symtab.insert_list (eq_fst (op =)) (key, (Tname, data))) constr_keys;
     4.9 -    val update_cases = Symtab.default (case_key, data);
    4.10 +    val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys;
    4.11 +    val update_cases = Symtab.update (case_key, data);
    4.12    in
    4.13      context
    4.14      |> map_constrs update_constrs
     5.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 17:35:59 2014 +0100
     5.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 17:36:00 2014 +0100
     5.3 @@ -39,7 +39,7 @@
     5.4    val ctr_sugars_of: Proof.context -> ctr_sugar list
     5.5    val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
     5.6    val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
     5.7 -  val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
     5.8 +  val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
     5.9  
    5.10    val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    5.11    val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    5.12 @@ -146,9 +146,9 @@
    5.13  
    5.14  fun register_ctr_sugar key ctr_sugar =
    5.15    Local_Theory.declaration {syntax = false, pervasive = true}
    5.16 -    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
    5.17 +    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)));
    5.18  
    5.19 -fun register_ctr_sugar_global key ctr_sugar =
    5.20 +fun default_register_ctr_sugar_global key ctr_sugar =
    5.21    Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    5.22  
    5.23  val isN = "is_";
     6.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Feb 12 17:35:59 2014 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Feb 12 17:36:00 2014 +0100
     6.3 @@ -130,7 +130,8 @@
     6.4            map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
     6.5       cases = cases |> fold Symtab.update
     6.6         (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
     6.7 -  fold (fn (key, info) => Ctr_Sugar.register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
     6.8 +  fold (fn (key, info) =>
     6.9 +    Ctr_Sugar.default_register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
    6.10  
    6.11  
    6.12  (* complex queries *)