# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID c2506f61fd267113bbf0039739bf9d70fb458e1a
# Parent  91bc9f69a95835492e143ab0a4cd17b250a7ffd6
generate 'fundec_cong' attribute for new-style (co)datatypes
* * *
compile

diff -r 91bc9f69a958 -r c2506f61fd26 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -206,6 +206,7 @@
 val id_def = @{thm id_def};
 val mp_conj = @{thm mp_conj};
 
+val fundefcong_attrs = @{attributes [fundef_cong]};
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
 val simp_attrs = @{attributes [simp]};
@@ -220,9 +221,7 @@
 fun flat_rec_arg_args xss =
   (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
      order. The second line is for compatibility with the old datatype package. *)
-(*
-  flat xss
-*)
+  (* flat xss *)
   map hd xss @ maps tl xss;
 
 fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss);
@@ -1248,7 +1247,7 @@
               (sel_bindingss, sel_defaultss))) lthy
           end;
 
-        fun derive_maps_sets_rels (ctr_sugar, lthy) =
+        fun derive_maps_sets_rels (ctr_sugar as {case_cong, ...} : ctr_sugar, lthy) =
           if live = 0 then
             ((([], [], [], []), ctr_sugar), lthy)
           else
@@ -1322,7 +1321,8 @@
                 join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
 
               val anonymous_notes =
-                [(map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms,
+                [([case_cong], fundefcong_attrs),
+                 (map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms,
                   code_nitpicksimp_attrs),
                  (map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
                     rel_inject_thms ms, code_nitpicksimp_attrs)]