
diff -r e2ab4147b244 -r fa37ee54644c src/HOL/Auth/Guard/Proto.thy
--- a/src/HOL/Auth/Guard/Proto.thy	Tue Dec 03 22:46:24 2024 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Fri Dec 06 13:33:25 2024 +0100
@@ -464,7 +464,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns1 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def keys_def, blast)
@@ -475,7 +475,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns1 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def, rule No_Nonce, simp)
@@ -493,7 +493,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s b" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.b" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns2 and R'=ns1 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def, rule No_Nonce, simp)
@@ -503,7 +503,7 @@
 apply (frule Guard_safe, simp)
 apply (frule Crypt_guard_invKey, simp)
 apply (frule_tac x=ns3b in ok_Guard, simp, simp, simp, clarsimp)
-apply (frule_tac K="pubK' s a" in Crypt_guard_invKey, simp)
+apply (frule_tac K="pubK' s Proto.a" in Crypt_guard_invKey, simp)
 apply (frule_tac R=ns2 and R'=ns2 and Ks=Ks and s=sa and s'=s in uniqD, simp+)
 apply (simp add: secret_def, simp add: secret_def, force, force)
 apply (simp add: secret_def keys_def, blast)




