diff -r 32b222d77fa0 -r 6746f5e1f1f8 thys/Exercises.thy
--- a/thys/Exercises.thy	Fri Aug 11 20:29:01 2017 +0100
+++ b/thys/Exercises.thy	Fri Aug 18 14:51:29 2017 +0100
@@ -49,7 +49,8 @@
 using Nil_is_append_conv apply blast
 apply blast
 apply(auto)
-using Star_string by fastforce
+using Star_cstring
+by (metis concat_eq_Nil_conv) 
 
 
 lemma atmostempty_correctness_aux:
@@ -78,7 +79,7 @@
   assumes "A \<subseteq> {[]}"
   shows "A\<star> \<subseteq> {[]}"
 using assms
-using Star_string concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce
+using Star_cstring concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce
 
 lemma Star_empty_string_finite:
   shows "finite ({[]}\<star>)"