src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55444 ec73f81e49e7
parent 55410 54b09e82b9e1
child 55464 56fa33537869
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 17:35:59 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 17:36:00 2014 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4    val ctr_sugars_of: Proof.context -> ctr_sugar list
     1.5    val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
     1.6    val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
     1.7 -  val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
     1.8 +  val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
     1.9  
    1.10    val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    1.11    val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    1.12 @@ -146,9 +146,9 @@
    1.13  
    1.14  fun register_ctr_sugar key ctr_sugar =
    1.15    Local_Theory.declaration {syntax = false, pervasive = true}
    1.16 -    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
    1.17 +    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)));
    1.18  
    1.19 -fun register_ctr_sugar_global key ctr_sugar =
    1.20 +fun default_register_ctr_sugar_global key ctr_sugar =
    1.21    Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    1.22  
    1.23  val isN = "is_";