1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 06 22:50:12 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Nov 06 23:05:44 2013 +0100
     1.3 @@ -1313,7 +1313,7 @@
     1.4    end;
     1.5  
     1.6  fun register_bnf key (bnf, lthy) =
     1.7 -  (bnf, Local_Theory.declaration {syntax = false, pervasive = false}
     1.8 +  (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
     1.9      (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy);
    1.10  
    1.11  fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Nov 06 22:50:12 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Nov 06 23:05:44 2013 +0100
     2.3 @@ -179,7 +179,7 @@
     2.4  (* TODO: register "sum" and "prod" as datatypes to enable N2M reduction for them *)
     2.5  
     2.6  fun register_fp_sugar key fp_sugar =
     2.7 -  Local_Theory.declaration {syntax = false, pervasive = false}
     2.8 +  Local_Theory.declaration {syntax = false, pervasive = true}
     2.9      (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
    2.10  
    2.11  fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss

     3.1 --- a/src/HOL/BNF/Tools/ctr_sugar.ML	Wed Nov 06 22:50:12 2013 +0100
     3.2 +++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Wed Nov 06 23:05:44 2013 +0100
     3.3 @@ -139,7 +139,7 @@
     3.4    Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
     3.5  
     3.6  fun register_ctr_sugar key ctr_sugar =
     3.7 -  Local_Theory.declaration {syntax = false, pervasive = false}
     3.8 +  Local_Theory.declaration {syntax = false, pervasive = true}
     3.9      (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
    3.10  
    3.11  val rep_compat_prefix = "new";
    3.12 @@ -918,7 +918,7 @@
    3.13          (ctr_sugar,
    3.14           lthy
    3.15           |> not rep_compat ?
    3.16 -            (Local_Theory.declaration {syntax = false, pervasive = false}
    3.17 +            (Local_Theory.declaration {syntax = false, pervasive = true}
    3.18                 (fn phi => Case_Translation.register
    3.19                    (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
    3.20           |> Local_Theory.notes (anonymous_notes @ notes) |> snd