--- a/Correctness.thy	Thu Feb 04 00:43:05 2016 +0000
+++ b/Correctness.thy	Thu Feb 04 14:45:30 2016 +0800
@@ -550,7 +550,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 cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
+         by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
         -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
               its @{term cp}-value equals @{term "preced th s"}, 
               which equals to @{term "?R"} by simplification: *}