use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)

--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Fri Aug 26 10:38:29 2011 -0700
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Wed Sep 08 16:10:49 2010 -0700
@@ -436,10 +436,10 @@
 apply(rule TrueI)+
 --{* Parallel *}     
       apply(simp add: SEM_def sem_def)
-      apply clarify
+      apply(clarify, rename_tac x y i Ts')
       apply(frule Parallel_length_post_PStar)
       apply clarify
-      apply(drule_tac j=xb in Parallel_Strong_Soundness)
+      apply(drule_tac j=i in Parallel_Strong_Soundness)
          apply clarify
         apply simp
        apply force