--- a/Implementation.thy	Thu Sep 21 14:33:13 2017 +0100
+++ b/Implementation.thy	Fri Sep 22 03:08:30 2017 +0100
@@ -82,7 +82,11 @@
   have [simp]: "preceds {th} s = {the_preced s th}"
     by (unfold the_preced_def, simp)
   show ?thesis 
-    by (unfold cp_rec cprecs_def, simp add:the_preced_def)
+    unfolding cprecs_def
+    apply(subst cp_rec)
+    apply(simp add: the_preced_def)  
+    done
+      
 qed    
 
 text {*
@@ -963,8 +967,11 @@
   equals its precedence:
 *}
 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"
- by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def)
-
+  unfolding  children_of_th
+  apply(subst vat_es.cp_rec)
+  apply(simp add:the_preced_def children_of_th)
+  done
+    
 end
 
 text {*