# HG changeset patch
# User blanchet
# Date 1436808175 -7200
# Node ID b88a1279c8eac5038cff56a46461d6ccc6f1cd76
# Parent  9a14d574ea65de4d2b02f4f220cee6440b6e8c38
tuning

diff -r 9a14d574ea65 -r b88a1279c8ea src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 13 19:22:50 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jul 13 19:22:55 2015 +0200
@@ -1520,11 +1520,13 @@
                 ((Binding.qualify true fun_name (Binding.name thmN), attrs), [(thms, [])]))
               fun_names (take actual_nn thmss))
           |> filter_out (null o fst o hd o snd);
+
+        val fun_ts0 = map fst def_infos;
       in
         lthy
-        |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat sel_thmss)
-        |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat ctr_thmss)
-        |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat code_thmss)
+        |> Spec_Rules.add Spec_Rules.Equational (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)
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes)
         |> snd
         |> (fn lthy =>