src/HOLCF/ex/Stream.thy

--- a/src/HOLCF/ex/Stream.thy	Wed Feb 20 14:52:38 2008 +0100
+++ b/src/HOLCF/ex/Stream.thy	Wed Feb 20 18:28:16 2008 +0100
@@ -433,7 +433,7 @@
 by (simp add: inat_defs split:inat_splits)
 
 lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
-by (simp add: ile_def slen_take_eq)
+by (simp add: linorder_not_less [symmetric] slen_take_eq)
 
 lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
 by (rule slen_take_eq_rev [THEN iffD1], auto)