# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID bf4188deabb20e091f7c8e19baaff2f1930d9b4e
# Parent  180f1b3508ed2ae3f235d1d75ecb99a086136116
rename_tac'd scripts

diff -r 180f1b3508ed -r bf4188deabb2 src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -217,13 +217,13 @@
 
 lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X"
 apply (induct X, simp_all)
-apply (rule_tac x="[Agent agent]" in exI, simp)
-apply (rule_tac x="[Number nat]" in exI, simp)
-apply (rule_tac x="[Nonce nat]" in exI, simp)
-apply (rule_tac x="[Key nat]" in exI, simp)
-apply (rule_tac x="[Hash X]" in exI, simp)
+apply (rename_tac agent, rule_tac x="[Agent agent]" in exI, simp)
+apply (rename_tac nat, rule_tac x="[Number nat]" in exI, simp)
+apply (rename_tac nat, rule_tac x="[Nonce nat]" in exI, simp)
+apply (rename_tac nat, rule_tac x="[Key nat]" in exI, simp)
+apply (rename_tac X, rule_tac x="[Hash X]" in exI, simp)
 apply (clarify, rule_tac x="l@la" in exI, simp)
-by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
+by (clarify, rename_tac nat X y, rule_tac x="[Crypt nat X]" in exI, simp)
 
 lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
 apply (induct l)
diff -r 180f1b3508ed -r bf4188deabb2 src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -211,13 +211,13 @@
 
 lemma kparts_msg_set: "EX l. kparts {X} = set l & cnb l = crypt_nb X"
 apply (induct X, simp_all)
-apply (rule_tac x="[Agent agent]" in exI, simp)
-apply (rule_tac x="[Number nat]" in exI, simp)
-apply (rule_tac x="[Nonce nat]" in exI, simp)
-apply (rule_tac x="[Key nat]" in exI, simp)
+apply (rename_tac agent, rule_tac x="[Agent agent]" in exI, simp)
+apply (rename_tac nat, rule_tac x="[Number nat]" in exI, simp)
+apply (rename_tac nat, rule_tac x="[Nonce nat]" in exI, simp)
+apply (rename_tac nat, rule_tac x="[Key nat]" in exI, simp)
 apply (rule_tac x="[Hash X]" in exI, simp)
 apply (clarify, rule_tac x="l@la" in exI, simp)
-by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
+by (clarify, rename_tac nat X y, rule_tac x="[Crypt nat X]" in exI, simp)
 
 lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
 apply (induct l)