src/HOL/BNF/Tools/ctr_sugar.ML

 
 fun ctr_sugars_of ctxt =
   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 = false}
+  Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
 
 val rep_compat_prefix = "new";
 
 val isN = "is_";

            case_conv_ifs = case_conv_if_thms};
       in
         (ctr_sugar,
          lthy
          |> not rep_compat ?
-            (Local_Theory.declaration {syntax = false, pervasive = false}
+            (Local_Theory.declaration {syntax = false, pervasive = true}
                (fn phi => Case_Translation.register
                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
          |> Local_Theory.notes (anonymous_notes @ notes) |> snd
          |> register_ctr_sugar fcT_name ctr_sugar)
       end;