--- a/Myhill_2.thy	Sat Feb 19 19:27:33 2011 +0000
+++ b/Myhill_2.thy	Sat Feb 19 20:15:59 2011 +0000
@@ -275,7 +275,7 @@
     by (rule rev_finite_subset) (auto)
 next
   show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
-    unfolding tag_str_ALT_def 
+    unfolding tag_str_ALT_def
     unfolding str_eq_def
     unfolding str_eq_rel_def
     by auto