1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Nov 06 22:50:12 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Nov 06 23:05:44 2013 +0100
     1.3 @@ -179,7 +179,7 @@
     1.4  (* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *)
     1.5  
     1.6  fun register_fp_sugar key fp_sugar =
     1.7 -  Local_Theory.declaration {syntax = false, pervasive = false}
     1.8 +  Local_Theory.declaration {syntax = false, pervasive = true}
     1.9      (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
    1.10  
    1.11  fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss