src/HOL/Hoare_Parallel/OG_Examples.thy

--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Wed Jun 11 14:24:23 2014 +1000
@@ -443,7 +443,7 @@
 apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
 --{* 9 subgoals left *}
 apply (force simp add:less_Suc_eq)
-apply(drule sym)
+apply(hypsubst_thin, drule sym)
 apply (force simp add:less_Suc_eq)+
 done