src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

   val fp_sugar_of_global: theory -> string -> fp_sugar option
   val fp_sugars_of: Proof.context -> fp_sugar list
   val fp_sugars_of_global: theory -> fp_sugar list
   val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) ->
     (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
-  val interpret_fp_sugars: fp_sugar list -> local_theory -> local_theory
+  val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
   val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
-  val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
+  val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
 
   val co_induct_of: 'a list -> 'a
   val strong_co_induct_of: 'a list -> 'a
 
   val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->

   fold (fn fp_sugar as {T = Type (s, _), ...} =>
       Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
     fp_sugars;
 
-fun register_fp_sugars fp_sugars =
-  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars fp_sugars;
+fun register_fp_sugars keep fp_sugars =
+  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars keep fp_sugars;
 
 fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
     live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
     common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
     rel_distinctss noted =

          co_rec_selss = nth co_rec_selsss kk, rel_injects = nth rel_injectss kk,
          rel_distincts = nth rel_distinctss kk}
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
   in
     register_fp_sugars_raw fp_sugars
-    #> fold interpret_bnf (#bnfs fp_res)
-    #> interpret_fp_sugars fp_sugars
+    #> fold (interpret_bnf (K true)) (#bnfs fp_res)
+    #> interpret_fp_sugars (K true) fp_sugars
   end;
 
 (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
    "x.x_A", "y.A"). *)
 fun quasi_unambiguous_case_names names =