# HG changeset patch
# User huffman
# Date 1267579203 28800
# Node ID a2a59e92b02eed4a5506226a0f53f88c9b2353d4
# Parent  cc57f4a274a35d939d3fb93524730c8f3db50619
variable name changed

diff -r cc57f4a274a3 -r a2a59e92b02e src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Tue Mar 02 16:25:59 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy	Tue Mar 02 17:20:03 2010 -0800
@@ -290,12 +290,12 @@
 
 lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
 apply (simp add: stream.finite_def,auto)
-apply (rule_tac x="Suc n" in exI)
+apply (rule_tac x="Suc i" in exI)
 by (simp add: stream_take_lemma4)
 
 lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
 apply (simp add: stream.finite_def, auto)
-apply (rule_tac x="n" in exI)
+apply (rule_tac x="i" in exI)
 by (erule stream_take_lemma3,simp)
 
 lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"