diff -r a0bcf886b8ef -r 8c4b6fb43ebe Regular_Set.thy
--- a/Regular_Set.thy	Fri Jul 05 12:07:48 2013 +0100
+++ b/Regular_Set.thy	Fri Jul 05 17:19:17 2013 +0100
@@ -216,7 +216,7 @@
 abbreviation 
   Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
 where
-  "Derivss s As \<equiv> \<Union> (Derivs s) ` As"
+  "Derivss s As \<equiv> \<Union> (Derivs s ` As)"
 
 
 lemma Deriv_empty[simp]:   "Deriv a {} = {}"