--- a/Correctness.thy	Wed Feb 03 14:37:35 2016 +0000
+++ b/Correctness.thy	Thu Feb 04 00:43:05 2016 +0000
@@ -406,7 +406,7 @@
       have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = 
             the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>
                             (\<exists> th'. n = Th th')}"
-      by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)
+        by (force)
       moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) 
       ultimately show ?thesis by simp
     qed