src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

       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 fp_sugars #> interpret_fp_sugars fp_sugars;
+  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars 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 =