diff --git a/src/pred_set/src/pred_setScript.sml b/src/pred_set/src/pred_setScript.sml
index 58dccd78c2..ca42fce419 100644
--- a/src/pred_set/src/pred_setScript.sml
+++ b/src/pred_set/src/pred_setScript.sml
@@ -7531,7 +7531,7 @@ Proof
 QED
 
 (* ----------------------------------------------------------------------
-    A proof of Koenig's Lemma
+    A proof of Kőnig's Lemma                                                UOK
    ---------------------------------------------------------------------- *)
 
 (* a counting exercise for R-trees.  If x0 has finitely many successors, and