--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 14:53:43 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 23 17:43:23 2013 +0200
@@ -764,7 +764,7 @@
@{thm list.discI(1)[no_vars]} \\
@{thm list.discI(2)[no_vars]}
-\item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.sel(1)[no_vars]} \\
@{thm list.sel(2)[no_vars]}
--- a/src/HOL/BNF/Examples/Stream.thy Mon Sep 23 14:53:43 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy Mon Sep 23 17:43:23 2013 +0200
@@ -33,7 +33,6 @@
*}
code_datatype Stream
-lemmas [code] = stream.sel stream.set stream.case
lemma stream_case_cert:
assumes "CASE \<equiv> stream_case c"
@@ -66,8 +65,6 @@
"shd (smap f s) = f (shd s)" "stl (smap f s) = smap f (stl s)"
by (case_tac [!] s) auto
-declare stream.map[code]
-
theorem shd_sset: "shd s \<in> sset s"
by (case_tac s) auto
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 23 14:53:43 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 23 17:43:23 2013 +0200
@@ -772,7 +772,7 @@
(expandN, expand_thms, []),
(injectN, inject_thms, iff_attrs @ induct_simp_attrs),
(nchotomyN, [nchotomy_thm], []),
- (selN, all_sel_thms, simp_attrs),
+ (selN, all_sel_thms, code_simp_attrs),
(splitN, [split_thm], []),
(split_asmN, [split_asm_thm], []),
(splitsN, [split_thm, split_asm_thm], []),