changeset 54285 | 578371ba74cc |
parent 54265 | 3e1d230f1c00 |
child 54421 | 632be352a5a3 |
--- a/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 06 22:50:12 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Nov 06 23:05:44 2013 +0100 @@ -1313,7 +1313,7 @@ end; fun register_bnf key (bnf, lthy) = - (bnf, Local_Theory.declaration {syntax = false, pervasive = false} + (bnf, Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.default (key, morph_bnf phi bnf))) lthy); fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =