diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -455,7 +455,7 @@
   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