--- a/Closures.thy	Fri Sep 02 13:29:46 2011 +0000
+++ b/Closures.thy	Fri Sep 02 13:30:17 2011 +0000
@@ -199,7 +199,7 @@
 qed
 
 lemma cofinite_regular:
-  fixes A::"('a::finite list) set"
+  fixes A::"'a::finite lang"
   assumes "finite (- A)"
   shows "regular A"
 proof -
@@ -278,9 +278,8 @@
   def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}"
   have b: "infinite B"
     unfolding infinite_iff_countable_subset
-    apply(rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI)
-    apply(auto simp add: inj_on_def B_def)
-    done
+    unfolding inj_on_def B_def
+    by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto)
   moreover
   have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" 
     apply(auto simp add: B_def A_def)