reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
authorblanchet
Fri Feb 07 10:44:04 2014 +0100 (2014-02-07)
changeset 553563ea8ace6bc8a
parent 55355 b5b64d9d1002
child 55357 1dd39517e1ce
reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Feb 07 00:48:04 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Feb 07 10:44:04 2014 +0100
     1.3 @@ -1307,7 +1307,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.update (key, morph_bnf phi bnf))) lthy);
     1.8 +    (fn phi => Data.map (Symtab.default (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	Fri Feb 07 00:48:04 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 07 10:44:04 2014 +0100
     2.3 @@ -180,7 +180,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.update (key, morph_fp_sugar phi fp_sugar)));
     2.8 +    (fn phi => Data.map (Symtab.default (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_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 07 00:48:04 2014 +0100
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 07 10:44:04 2014 +0100
     3.3 @@ -152,10 +152,10 @@
     3.4  
     3.5  fun register_ctr_sugar key ctr_sugar =
     3.6    Local_Theory.declaration {syntax = false, pervasive = true}
     3.7 -    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)));
     3.8 +    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
     3.9  
    3.10  fun register_ctr_sugar_global key ctr_sugar =
    3.11 -  Context.theory_map (Data.map (Symtab.update (key, ctr_sugar)));
    3.12 +  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    3.13  
    3.14  val rep_compat_prefix = "new";
    3.15