# HG changeset patch
# User blanchet
# Date 1379932834 -7200
# Node ID 6a4e3299dfd17e6d5a428a066d4ddd1f48914258
# Parent  576f9637dc7a10dd974bbf397639bc0e5a8d0016
set [code] on case equations

diff -r 576f9637dc7a -r 6a4e3299dfd1 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 23 10:58:37 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 23 12:40:34 2013 +0200
@@ -729,7 +729,7 @@
 \begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{case} @{text "[simp]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.case(1)[no_vars]} \\
 @{thm list.case(2)[no_vars]}
 
@@ -802,19 +802,19 @@
 \begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{set} @{text "[code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.set(1)[no_vars]} \\
 @{thm list.set(2)[no_vars]}
 
-\item[@{text "t."}\hthm{map} @{text "[code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.map(1)[no_vars]} \\
 @{thm list.map(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel\_inject} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.rel_inject(1)[no_vars]} \\
 @{thm list.rel_inject(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.rel_distinct(1)[no_vars]} \\
 @{thm list.rel_distinct(2)[no_vars]}
 
@@ -839,11 +839,11 @@
 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
 prove $m$ properties simultaneously.
 
-\item[@{text "t."}\hthm{fold} @{text "[code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.fold(1)[no_vars]} \\
 @{thm list.fold(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rec} @{text "[code]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.rec(1)[no_vars]} \\
 @{thm list.rec(2)[no_vars]}
 
diff -r 576f9637dc7a -r 6a4e3299dfd1 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Sep 23 10:58:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Sep 23 12:40:34 2013 +0200
@@ -133,6 +133,7 @@
 val iff_attrs = @{attributes [iff]};
 val induct_simp_attrs = @{attributes [induct_simp]};
 val simp_attrs = @{attributes [simp]};
+val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
 
 fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
 
@@ -758,7 +759,7 @@
         val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
 
         val notes =
-          [(caseN, case_thms, simp_attrs),
+          [(caseN, case_thms, code_simp_attrs),
            (case_congN, [case_cong_thm], []),
            (case_convN, case_conv_thms, []),
            (collapseN, safe_collapse_thms, simp_attrs),