diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Guard/Proto.thy
--- a/src/HOL/Auth/Guard/Proto.thy	Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy	Thu Oct 13 16:09:31 2022 +0100
@@ -122,7 +122,7 @@
 by (unfold has_only_Says'_def is_Says_def, blast)
 
 lemma has_only_Says_tr [simp]: "has_only_Says' p \<Longrightarrow> has_only_Says (tr p)"
-apply (unfold has_only_Says_def)
+unfolding has_only_Says_def
 apply (rule allI, rule allI, rule impI)
 apply (erule tr.induct)
 apply (auto simp: has_only_Says'_def ok_def)
@@ -354,7 +354,7 @@
 by (unfold uniq'_def, blast)
 
 lemma uniq'_imp_uniq: "\<lbrakk>uniq' p inff secret; ord p inff\<rbrakk> \<Longrightarrow> uniq p secret"
-apply (unfold uniq_def)
+unfolding uniq_def
 apply (rule allI)+
 apply (case_tac "inff R R'")
 apply (blast dest: uniq'D)
@@ -442,7 +442,7 @@
 subsection\<open>guardedness for NSL\<close>
 
 lemma "uniq ns secret \<Longrightarrow> preserv ns keys n Ks"
-apply (unfold preserv_def)
+unfolding preserv_def
 apply (rule allI)+
 apply (rule impI, rule impI, rule impI, rule impI, rule impI)
 apply (erule fresh_ruleD, simp, simp, simp, simp)