--- a/Correctness.thy	Tue Jun 14 15:06:16 2016 +0100
+++ b/Correctness.thy	Fri Jun 17 09:46:25 2016 +0100
@@ -558,7 +558,7 @@
               of it contains only itself, so, its @{term cp}-value
               equals its @{term preced}-value: *}
         have "?L = cp (t@s) th'"
-         by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
+          by (simp add: detached_cp_preced eq_pv vat_t.detached_intro)
         -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion},
               its @{term cp}-value equals @{term "preced th s"}, 
               which equals to @{term "?R"} by simplification: *}