# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 4a6c9bcb418941815fd434518d534596e4642f4c
# Parent  d4c06c99a4dca94f489ce3a6ddf0c397ad6b79d2
set 'fundef_cong' attribute also for (co)datatypes with no live type variables

diff -r d4c06c99a4dc -r 4a6c9bcb4189 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -1464,13 +1464,20 @@
 
             fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
             val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
+
+            val (ctr_sugar as {case_cong, ...}, lthy') =
+              free_constructors tacss ((((plugins, discs_sels), standard_binding), ctr_specs),
+                sel_default_eqs) lthy
+
+            val anonymous_notes =
+              [([case_cong], fundefcong_attrs)]
+              |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
           in
-            free_constructors tacss ((((plugins, discs_sels), standard_binding), ctr_specs),
-              sel_default_eqs) lthy
+            (ctr_sugar, lthy' |> Local_Theory.notes anonymous_notes |> snd)
           end;
 
-        fun derive_map_set_rel_thms (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs,
-            exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss,
+        fun derive_map_set_rel_thms (ctr_sugar as {casex, case_thms, discs, selss, ctrs, exhaust,
+            exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss,
             ...} : ctr_sugar, lthy) =
           if live = 0 then
             ((([], [], [], []), ctr_sugar), lthy)
@@ -1583,9 +1590,7 @@
                   rel_inject_thms ms;
 
               val ctr_transfer_thms =
-                let
-                  val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs;
-                in
+                let val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs in
                   Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                     (K (mk_ctr_transfer_tac rel_intro_thms))
                   |> Conjunction.elim_balanced (length goals)
@@ -1919,8 +1924,7 @@
                 end;
 
               val anonymous_notes =
-                [([case_cong], fundefcong_attrs),
-                 (rel_eq_thms, code_nitpicksimp_attrs)]
+                [(rel_eq_thms, code_nitpicksimp_attrs)]
                 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
               val notes =