diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Library/Stream.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -491,9 +491,8 @@
 
 lemma sinterleave_snth[simp]:
   "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
-   "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
-  by (induct n arbitrary: s1 s2)
-    (auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2])
+  "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
+  by (induct n arbitrary: s1 s2) simp_all
 
 lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2"
 proof (intro equalityI subsetI)