src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55356 3ea8ace6bc8a
parent 55347 a87e49f4336d
child 55394 d5ebe055b599
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 07 00:48:04 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 07 10:44:04 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.update (key, morph_ctr_sugar phi ctr_sugar)));
     1.8 +    (fn phi => Data.map (Symtab.default (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.update (key, ctr_sugar)));
    1.12 +  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
    1.13  
    1.14  val rep_compat_prefix = "new";
    1.15