# HG changeset patch
# User huffman
# Date 1283987449 25200
# Node ID 5e681762d53896849d2d2b0cc438147a9c8464b9
# Parent  002b431171154dfd4b0805895d3281601fab6050
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)

diff -r 002b43117115 -r 5e681762d538 src/HOL/Hoare_Parallel/OG_Hoare.thy
--- 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