--- a/Closures.thy	Thu Jul 28 17:52:36 2011 +0000
+++ b/Closures.thy	Sun Jul 31 10:27:41 2011 +0000
@@ -48,7 +48,7 @@
   shows "regular (- A)"
 proof -
   from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode)
-  then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def)
+  then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_def)
   then show "regular (- A)" by (simp add: Myhill_Nerode)
 qed