diff --git a/doc/examples/phoas.lean b/doc/examples/phoas.lean
index 5f8413646e..019b6a985e 100644
--- a/doc/examples/phoas.lean
+++ b/doc/examples/phoas.lean
@@ -61,7 +61,8 @@ We write the final type of a closed term using polymorphic quantification over a
 choices of `rep` type family
 -/
 
-open Ty Term'
+open Ty (nat fn)
+open Term'
 
 namespace FirstTry