diff -r b73478aaf33e -r f6a603be52d6 Closures.thy
--- a/Closures.thy	Tue Aug 09 22:15:11 2011 +0000
+++ b/Closures.thy	Thu Aug 11 10:26:19 2011 +0000
@@ -153,7 +153,7 @@
   have fin: "finite (pders_lang B r)" by (rule finite_pders_lang)
   
   have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"
-    by (simp add: Ders_pders)
+    by (simp add: Ders_pders pders_lang_def)
   also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp
   finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq
     by simp