--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Dec 02 15:04:38 2019 +0100
@@ -1533,9 +1533,10 @@
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