diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/HOLCF/Library/Stream.thy
--- a/src/HOL/HOLCF/Library/Stream.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/HOLCF/Library/Stream.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -361,7 +361,7 @@
 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
 by (cases x) auto
 
-lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y \<and> a \<noteq> \<bottom> \<and> enat n < #y)"
+lemma slen_scons_eq: "(enat (Suc n) < #x) = (\<exists>a y. x = a && y \<and> a \<noteq> \<bottom> \<and> enat n < #y)"
 apply (auto, case_tac "x=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (case_tac "#y") apply simp_all