--- a/Implementation.thy	Tue Jul 12 15:09:09 2016 +0100
+++ b/Implementation.thy	Tue Aug 16 11:49:37 2016 +0100
@@ -463,7 +463,8 @@
             assume "x \<in> Range {(Th th, Th holder)}"
             hence eq_x: "x = Th holder" using RangeE by auto
             show False
-            proof(cases rule:vat_es.ancestors_headE[OF assms(1) start])
+            find_theorems ancestors tRAG
+            proof(cases rule:vat_es.forest_s.ancestors_headE[OF assms(1) start])
               case 1
               from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG
               show ?thesis by (auto simp:ancestors_def acyclic_def)