# HG changeset patch
# User wenzelm
# Date 1575128794 -3600
# Node ID 95e12ecdcb5f558ac78b8bada7b4d399e60ce086
# Parent  abb0d984abbc4c6a2beca71490f1986f3e434c2e
proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";

diff -r abb0d984abbc -r 95e12ecdcb5f src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Nov 30 16:42:15 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Nov 30 16:46:34 2019 +0100
@@ -2154,10 +2154,10 @@
       in
         lthy11
 (* TODO:
-        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat sel_thmss)
-        |> Spec_Rules.add Spec_Rules.equational ([fun_t0], flat ctr_thmss)
+        |> 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_lhs0] [code_thm]
+        |> Spec_Rules.add "" Spec_Rules.equational [fun_lhs] [code_thm]
         |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd