--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Oct 13 18:45:48 2014 +0200
@@ -451,10 +451,8 @@
end;
fun interpretation name prefs f =
- let val new_f = new_interpretation_of prefs f in
- Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
- #> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f)
- end;
+ 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]};