--- a/Closures.thy	Thu Aug 11 16:55:41 2011 +0000
+++ b/Closures.thy	Thu Aug 11 23:11:39 2011 +0000
@@ -143,7 +143,7 @@
 subsection {* Closure under left-quotients *}
 
 abbreviation
-  "Ders_lang A B \<equiv> \<Union>s \<in> A. Ders s B"
+  "Ders_lang A B \<equiv> \<Union>x \<in> A. Ders x B"
 
 lemma closure_left_quotient:
   assumes "regular A"