--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Apr 11 08:44:41 2009 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Apr 13 09:29:55 2009 -0700
@@ -288,8 +288,7 @@
lemma Cons_not_UU: "a>>s ~= UU"
apply (subst Consq_def2)
-apply (rule seq.con_rews)
-apply (rule Def_not_UU)
+apply simp
done