diff --git a/ITP/geometry.tex b/ITP/geometry.tex
index 47d8128..50b7276 100644
--- a/ITP/geometry.tex
+++ b/ITP/geometry.tex
@@ -26,7 +26,7 @@
 
 \begin{lstlisting}
 theorem hole_6_theorem : ∀ (pts : Finset Point),
-    Point.SetInGenPos pts → pts.card = 30 → HasEmptyKGon 6 pts
+    SetInGenPos pts → pts.card = 30 → HasEmptyKGon 6 pts
 \end{lstlisting}
 
 At the root  of the encoding of Heule and Scheucher is the idea that