--- a/Correctness.thy	Wed Jan 27 13:50:02 2016 +0000
+++ b/Correctness.thy	Thu Jan 28 13:46:45 2016 +0000
@@ -730,9 +730,9 @@
 *}
 
 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-  assumes "th \<notin> runing (t@s)"
+  assumes "th \<notin> runing (t @ s)"
   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-                    "th' \<in> runing (t@s)"
+                    "th' \<in> runing (t @ s)"
 proof -
   -- {* According to @{thm vat_t.th_chain_to_ready}, either 
         @{term "th"} is in @{term "readys"} or there is path leading from it to