diff -r 1cf129590be8 -r 24106dc44def src/HOL/Hoare_Parallel/OG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -111,7 +111,8 @@
 apply(rule conjI)
  apply (blast dest: L3_5i)
 apply(simp add: SEM_def sem_def id_def)
-apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow)
+apply (auto dest: Basic_ntran rtrancl_imp_UN_relpow)
+apply blast
 done
 
 lemma atom_hoare_sound [rule_format]: