diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Public.thy	Thu Oct 13 16:09:31 2022 +0100
@@ -255,7 +255,7 @@
   that expression is not in normal form.\<close>
 
 lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
-apply (unfold keysFor_def)
+unfolding keysFor_def
 apply (induct_tac "C")
 apply (auto intro: range_eqI)
 done