src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

           |> filter_out (null o fst o hd o snd);
 
         val fun_ts0 = map fst def_infos;
       in
         lthy
-        |> Spec_Rules.add "" (Spec_Rules.equational_primcorec primcorec_types) fun_ts0 (flat sel_thmss)
-        |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat ctr_thmss)
-        |> Spec_Rules.add "" Spec_Rules.equational fun_ts0 (flat code_thmss)
+        |> Spec_Rules.add Binding.empty (Spec_Rules.equational_primcorec primcorec_types)
+            fun_ts0 (flat sel_thmss)
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat ctr_thmss)
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational fun_ts0 (flat code_thmss)
         |> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat code_thmss))
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
         |> snd
         |> (fn lthy =>
           let