--- a/Closures.thy	Fri Sep 02 13:34:45 2011 +0000
+++ b/Closures.thy	Fri Sep 02 14:01:11 2011 +0000
@@ -285,7 +285,6 @@
     apply(auto simp add: B_def A_def)
     apply(auto simp add: str_eq_def)
     apply(drule_tac x="CHR ''b'' ^^^ aa" in spec)
-    (*apply(auto simp add: f_def dest: l3)*)
     apply(auto)
     apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test)
     apply(simp add: length_test_def)