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 Binding.empty Spec_Rules.equational size_consts size_simps
+        |> Spec_Rules.add Binding.empty 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;