src/HOL/Tools/BNF/bnf_lfp_compat.ML

 
 fun interpretation name prefs f =
   Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
   #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f);
 
-val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
+val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib Code.Equation :: @{attributes [nitpick_simp, simp]};
 
 fun datatype_compat fpT_names lthy =
   let
     val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
       mk_infos_of_mutually_recursive_new_datatypes [] eq_set fpT_names lthy;