diff -r f270cd6ee185 -r c5b398584f5e src/HOL/Examples/Functions.thy
--- a/src/HOL/Examples/Functions.thy	Fri Oct 18 14:37:09 2024 +0200
+++ b/src/HOL/Examples/Functions.thy	Fri Oct 18 15:36:42 2024 +0200
@@ -333,7 +333,7 @@
     (if n \<le> 1 then Some [n]
      else if even n
        then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
-       else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
+       else do { ns \<leftarrow> collatz (3 * n + 1); Some (n # ns)})"
 
 declare collatz.simps[code]
 value "collatz 23"