diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean
index 82ae8170fb..54db73fb4c 100644
--- a/src/Lean/Util/CollectLevelParams.lean
+++ b/src/Lean/Util/CollectLevelParams.lean
@@ -31,6 +31,9 @@ mutual
     | _          => id
 end
 
+def visitLevels (us : List Level) : Visitor :=
+  fun s => us.foldl (fun s u => visitLevel u s) s
+
 mutual
   partial def visitExpr (e : Expr) : Visitor := fun s =>
     if !e.hasLevelParam then s
@@ -44,7 +47,7 @@ mutual
     | .letE _ t v b _  => visitExpr b ∘ visitExpr v ∘ visitExpr t
     | .app f a         => visitExpr a ∘ visitExpr f
     | .mdata _ b       => visitExpr b
-    | .const _ us      => fun s => us.foldl (fun s u => visitLevel u s) s
+    | .const _ us      => visitLevels us
     | .sort u          => visitLevel u
     | _                => id
 end