--- a/Myhill_1.thy	Wed Feb 09 04:54:23 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 09 06:09:46 2011 +0000
@@ -271,7 +271,7 @@
 overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"
 begin
 fun
-  L_rexp :: "rexp \<Rightarrow> string set"
+  L_rexp :: "rexp \<Rightarrow> lang"
 where
     "L_rexp (NULL) = {}"
   | "L_rexp (EMPTY) = {[]}"
@@ -281,6 +281,7 @@
   | "L_rexp (STAR r) = (L_rexp r)\<star>"
 end
 
+
 text {* ALT-combination of a set or regulare expressions *}
 
 abbreviation
@@ -293,6 +294,7 @@
 *}
 
 lemma folds_alt_simp [simp]:
+  fixes rs::"rexp set"
   assumes a: "finite rs"
   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
 apply(rule set_eqI)