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