diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 7f99cefe22..41ed319700 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -203,6 +203,12 @@ def take : Nat → List α → List α
   | n+1, []    => []
   | n+1, a::as => a :: take n as
 
+def takeWhile (p : α → Bool) : List α → List α
+  | []       => []
+  | hd :: tl => match p hd with
+   | true  => hd :: takeWhile p tl
+   | false => []
+
 @[specialize] def foldr (f : α → β → β) (init : β) : List α → β
   | []     => init
   | a :: l => f a (foldr f init l)
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
index 6146ff5306..afc2036b84 100644
--- a/src/Lean/Server/Utils.lean
+++ b/src/Lean/Server/Utils.lean
@@ -155,15 +155,5 @@ def publishProgressDone (m : DocumentMeta) (hOut : FS.Stream) : IO Unit :=
 
 end Lean.Server
 
-namespace List
-
-universe u
-
-def takeWhile (p : α → Bool) : List α → List α
-  | []       => []
-  | hd :: tl => if p hd then hd :: takeWhile p tl else []
-
-end List
-
 def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) : Lean.Lsp.Range :=
   ⟨text.utf8PosToLspPos r.start, text.utf8PosToLspPos r.stop⟩