src/HOLCF/IOA/meta_theory/Seq.thy

--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -8,7 +8,9 @@
 imports HOLCF
 begin
 
-domain 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
+default_sort pcpo
+
+domain (unsafe) 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
 
 (*
    sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"