--- a/Nominal/nominal_termination.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_termination.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -25,7 +25,7 @@
 
 val simp_attribs = map (Attrib.internal o K)
   [Simplifier.simp_add,
-   Code.add_default_eqn_attribute,
+   Code.add_default_eqn_attribute Code.Equation,
    Named_Theorems.add @{named_theorems nitpick_simp}]
 
 val eqvt_attrib =  Attrib.internal (K Nominal_ThmDecls.eqvt_add)