# HG changeset patch
# User wenzelm
# Date 1131386582 -3600
# Node ID 94b528311e22e7993f605af2993b573345cdd664
# Parent  1e4516e68a582cddb4250dffd61a3c1ac924022d
avoid 'as' as identifier;

diff -r 1e4516e68a58 -r 94b528311e22 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Mon Nov 07 18:50:53 2005 +0100
+++ b/src/HOLCF/ex/Stream.thy	Mon Nov 07 19:03:02 2005 +0100
@@ -71,7 +71,7 @@
 lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)"
 by (auto,insert stream.exhaust [of x],auto)
 
-lemma stream_neq_UU: "x~=UU ==> EX a as. x=a&&as & a~=UU"
+lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU"
 by (simp add: stream_exhaust_eq,auto)
 
 lemma stream_inject_eq [simp]: