--- a/Myhill_1.thy	Fri Jan 28 11:52:11 2011 +0000
+++ b/Myhill_1.thy	Fri Jan 28 12:53:01 2011 +0000
@@ -32,7 +32,7 @@
   Sequential composition of two languages @{text "L1"} and @{text "L2"} 
 *}
 
-definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
+definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100)
 where 
   "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"