--- a/src/HOLCF/IOA/meta_theory/Seq.thy Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
*)
-Seq = HOLCF +
+Seq = HOLCF + Inductive +
domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (infixr 65)