--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Dec 02 15:04:38 2019 +0100
@@ -1414,10 +1414,13 @@
|> massage_simple_notes fp_b_name;
val (noted, lthy') = lthy
- |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) map_thms)
+ |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+ (`(single o lhs_head_of o hd) map_thms)
|> fp = Least_FP ?
- uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) rel_code_thms)
- |> uncurry (Spec_Rules.add "" Spec_Rules.equational) (`(single o lhs_head_of o hd) set0_thms)
+ uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+ (`(single o lhs_head_of o hd) rel_code_thms)
+ |> uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational)
+ (`(single o lhs_head_of o hd) set0_thms)
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (rel_code_thms @ map_thms @ set_thms))
|> Local_Theory.notes (anonymous_notes @ notes);
@@ -2689,7 +2692,7 @@
|> massage_multi_notes fp_b_names fpTs;
in
lthy
- |> Spec_Rules.add "" Spec_Rules.equational recs (flat rec_thmss)
+ |> Spec_Rules.add Binding.empty Spec_Rules.equational recs (flat rec_thmss)
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat rec_thmss))
|> Local_Theory.notes (common_notes @ notes)
(* for "datatype_realizer.ML": *)
@@ -2869,7 +2872,7 @@
|> massage_multi_notes fp_b_names fpTs;
in
lthy
- |> fold (Spec_Rules.add "" Spec_Rules.equational corecs)
+ |> fold (Spec_Rules.add Binding.empty Spec_Rules.equational corecs)
[flat corec_sel_thmss, flat corec_thmss]
|> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) corec_code_thms)
|> Local_Theory.notes (common_notes @ notes)