# HG changeset patch
# User traytel
# Date 1366798506 -7200
# Node ID 199ce8cf604c19dd7d26e120f39164967558fc35
# Parent  c45ca48b526eeff352a2f6cf4e9ee048dd1992a4
took out workaround for bug fixed in 5af40820948b

diff -r c45ca48b526e -r 199ce8cf604c src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Wed Apr 24 11:36:11 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Wed Apr 24 12:15:06 2013 +0200
@@ -64,8 +64,7 @@
   unfolding shd_def stl_def stream_case_def stream_map_def stream.dtor_unfold
   by (case_tac [!] s) (auto simp: Stream_def stream.dtor_ctor)
 
-lemma stream_map_Stream[simp, code]: "stream_map f (x ## s) = f x ## stream_map f s"
-  by (metis stream.exhaust stream.sels stream_map_simps)
+declare stream.map[code]
 
 theorem shd_stream_set: "shd s \<in> stream_set s"
   by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta)