compile

--- a/src/HOL/BNF/Examples/Stream.thy	Thu Apr 25 17:13:24 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Apr 25 17:25:10 2013 +0200
@@ -197,7 +197,7 @@
 proof
   assume ?R
   thus ?L 
-    by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>n. s1 = smap f (sdrop n s) \<and> s2 = sdrop n s'"])
+    by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>n. s1 = smap f (sdrop n s) \<and> s2 = sdrop n s'", consumes 0])
       (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
 qed auto