# HG changeset patch
# User blanchet
# Date 1379951003 -7200
# Node ID 4163160853fde047027a87d56e9faf4e8694af46
# Parent  58d1b63bea81e4f596635460d1ba9c51aa49807f
added [code] to selectors

diff -r 58d1b63bea81 -r 4163160853fd src/Doc/Datatypes/Datatypes.thy
--- 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]}
 
diff -r 58d1b63bea81 -r 4163160853fd src/HOL/BNF/Examples/Stream.thy
--- 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
 
diff -r 58d1b63bea81 -r 4163160853fd src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- 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], []),