# HG changeset patch
# User blanchet
# Date 1366903510 -7200
# Node ID 273e7a90b16774befaf6aac3a55715eb78fd6969
# Parent  190f89980f7b60100fee9269795578ba446222fb
compile

diff -r 190f89980f7b -r 273e7a90b167 src/HOL/BNF/Examples/Stream.thy
--- 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