# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 85b13d75b2e4c477fe0d71a596052851ca8b8cd8
# Parent  10bd5ba8c9e6abc8eb5f73b3fdacd9c36eb75e32
rename_tac'd scrips

diff -r 10bd5ba8c9e6 -r 85b13d75b2e4 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -237,7 +237,7 @@
 apply fast
 
 apply (erule thin_rl)
-apply (rule_tac Q = "\<lambda>a s. \<exists>n. Z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
+apply (rename_tac expr1 u v Z, rule_tac Q = "\<lambda>a s. \<exists>n. Z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
 apply  (drule spec)
 apply  (erule eConseq2)
 apply  fast
@@ -267,6 +267,7 @@
 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc])
 apply fast
 
+apply (rename_tac expr1 u expr2 Z)
 apply (rule_tac R = "\<lambda>a v s. \<exists>n1 n2 t. Z -expr1\<succ>a-n1\<rightarrow> t \<and> t -expr2\<succ>v-n2\<rightarrow> s" in
                 hoare_ehoare.Call)
 apply   (erule spec)