--- a/Regular_Exp.thy	Fri Aug 19 20:39:07 2011 +0000
+++ b/Regular_Exp.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -16,7 +16,7 @@
   Times "('a rexp)" "('a rexp)" |
   Star "('a rexp)"
 
-primrec lang :: "'a rexp => 'a list set" where
+primrec lang :: "'a rexp => 'a lang" where
 "lang Zero = {}" |
 "lang One = {[]}" |
 "lang (Atom a) = {[a]}" |