Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
changeset 71214 5727bcc3c47c
parent 71205 95e12ecdcb5f
child 71376 26801434d628 
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -2157,7 +2157,7 @@
         |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.equational ([fun_lhs], flat ctr_thmss)
 *)
-        |> Spec_Rules.add "" Spec_Rules.equational [fun_lhs] [code_thm]
+        |> Spec_Rules.add Binding.empty Spec_Rules.equational [fun_lhs] [code_thm]
         |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd
isabelle