--- 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