diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -39,10 +39,14 @@
   "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
 by (cases xq) auto
 
-lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
-  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
-apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) 
-apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
+lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
+  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
+apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
+apply (cases yq) apply (auto simp add: equal_eq) done
+
+lemma [code nbe]:
+  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 lemma seq_case [code]:
   "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"