diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean
index 2b417436fc..e4882371b9 100644
--- a/src/Lean/Util/CollectLevelParams.lean
+++ b/src/Lean/Util/CollectLevelParams.lean
@@ -61,4 +61,7 @@ end CollectLevelParams
 def collectLevelParams (s : CollectLevelParams.State) (e : Expr) : CollectLevelParams.State :=
 CollectLevelParams.main e s
 
+def CollectLevelParams.State.collect (s : CollectLevelParams.State) (e : Expr) : CollectLevelParams.State :=
+collectLevelParams s e
+
 end Lean