--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -86,6 +86,6 @@
 lemma issued_nil: "issued [] = {Key0}"
 by (auto simp add: initk_def)
 
-lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
+lemmas issued_simps [code, code_pred_def] = issued_nil issued.simps(2)
 
 end