--- a/src/HOL/BNF/Tools/ctr_sugar.ML Tue Nov 05 09:45:03 2013 +0100
+++ b/src/HOL/BNF/Tools/ctr_sugar.ML Tue Nov 05 11:17:42 2013 +0100
@@ -139,7 +139,7 @@
Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
fun register_ctr_sugar key ctr_sugar =
- Local_Theory.declaration {syntax = false, pervasive = true}
+ Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
val rep_compat_prefix = "new";
@@ -918,7 +918,7 @@
(ctr_sugar,
lthy
|> not rep_compat ?
- (Local_Theory.declaration {syntax = false, pervasive = true}
+ (Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => Case_Translation.register
(Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
|> Local_Theory.notes (anonymous_notes @ notes) |> snd