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 =