src/HOL/Tools/BNF/bnf_lfp_size.ML

          (size_neqN, size_neq_thmss, [])]
         |> massage_multi_notes;
 
       val (noted, lthy3) =
         lthy2
-        |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
-        |> Spec_Rules.add Spec_Rules.Equational (overloaded_size_consts, overloaded_size_simps)
+        |> Spec_Rules.add Spec_Rules.equational (size_consts, size_simps)
+        |> Spec_Rules.add Spec_Rules.equational (overloaded_size_consts, overloaded_size_simps)
         |> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
           (*Ideally, this would be issued only if the "code" plugin is enabled.*)
         |> Local_Theory.notes notes;
 
       val phi0 = substitute_noted_thm noted;