--- a/thys/Spec.thy	Tue Oct 10 10:40:44 2017 +0100
+++ b/thys/Spec.thy	Tue Oct 10 11:31:47 2017 +0100
@@ -376,7 +376,7 @@
   fix s::"char list"
   assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')"
   then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')"
-    by (auto simp add: strict_suffix_def) 
+    by (force simp add: strict_suffix_def suffix_def) 
   define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)"
   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
   define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
@@ -404,7 +404,8 @@
   apply(rule conjI)
   apply(rule_tac x="flats list" in exI)
   apply(simp)
-  apply(blast)
+   apply(blast)
+  apply(simp add: suffix_def)
   using Prf.intros(6) by blast  
   ultimately
   show "finite (LV (STAR r) s)" by (simp add: finite_subset)

--- a/thys/SpecExt.thy	Tue Oct 10 10:40:44 2017 +0100
+++ b/thys/SpecExt.thy	Tue Oct 10 11:31:47 2017 +0100
@@ -885,7 +885,8 @@
   fix s::"char list"
   assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')"
   then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')"
-    by (auto simp add: strict_suffix_def) 
+    apply(auto simp add: strict_suffix_def suffix_def)
+    by force    
   define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)"
   define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
   define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. LV (STAR r) s2"
@@ -912,9 +913,8 @@
   apply(rule exI)
   apply(rule conjI)
   apply(rule_tac x="flats list" in exI)
-  apply(rule conjI)
-  apply(rule_tac x="flat a" in exI)
-  apply(simp)
+   apply(rule conjI)
+  apply(simp add: suffix_def)
   apply(blast)
   using Prf.intros(6) flat_Stars by blast  
   ultimately