diff -r 07b3112e464b -r 31cbcb019003 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Wed Feb 17 08:19:46 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy	Wed Feb 17 09:08:58 2010 -0800
@@ -54,8 +54,6 @@
                         | \<infinity>    \<Rightarrow> s1)"
 
 
-declare stream.rews [simp add]
-
 (* ----------------------------------------------------------------------- *)
 (* theorems about scons                                                    *)
 (* ----------------------------------------------------------------------- *)
@@ -149,13 +147,13 @@
 apply (insert stream.reach [of s], erule subst) back
 apply (simp add: fix_def2 stream.take_def)
 apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym])
-by (simp add: chain_iterate)
+by simp
 
 lemma chain_stream_take: "chain (%i. stream_take i$s)"
 apply (rule chainI)
 apply (rule monofun_cfun_fun)
 apply (simp add: stream.take_def del: iterate_Suc)
-by (rule chainE, simp add: chain_iterate)
+by (rule chainE, simp)
 
 lemma stream_take_prefix [simp]: "stream_take n$s << s"
 apply (insert stream_reach2 [of s])