diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 80e1a04fb9..81d9b5493c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -237,7 +237,7 @@ def mvarName (mvar : Expr) : MetaM Name := do
 def containsBadMax : Level → Bool
   | Level.succ u ..   => containsBadMax u
   | Level.max u v ..  => (u.hasParam && v.hasParam) || containsBadMax u || containsBadMax v
-  | Level.imax u v .. => containsBadMax u || containsBadMax v
+  | Level.imax u v .. => (u.hasParam && v.hasParam) || containsBadMax u || containsBadMax v
   | _                 => false
 
 open SubExpr