src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55347 a87e49f4336d
parent 55342 1bd9e637ac9f
child 55356 3ea8ace6bc8a
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Feb 06 13:04:06 2014 +0000
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Feb 06 17:05:47 2014 +0100
     1.3 @@ -152,10 +152,10 @@
     1.4  
     1.5  fun register_ctr_sugar key ctr_sugar =
     1.6    Local_Theory.declaration {syntax = false, pervasive = true}
     1.7 -    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
     1.8 +    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)));
     1.9  
    1.10  fun register_ctr_sugar_global key ctr_sugar =
    1.11 -  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    1.12 +  Context.theory_map (Data.map (Symtab.update (key, ctr_sugar)));
    1.13  
    1.14  val rep_compat_prefix = "new";
    1.15