diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 303823c3c9..344cd9a7f0 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -396,25 +396,23 @@ partial def splitOn (s : Substring) (sep : String := " ") : List Substring :=
   if sep == "" then
     [s]
   else
-    let stopPos := s.stopPos
-    let str     := s.str
     let rec loop (b i j : String.Pos) (r : List Substring) : List Substring :=
-      if i == stopPos then
+      if i == s.bsize then
         let r := if sep.atEnd j then
-          "".toSubstring::{ str := str, startPos := b, stopPos := i-j } :: r
+          "".toSubstring :: s.extract b (i-j) :: r
         else
-          { str := str, startPos := b, stopPos := i } :: r
+          s.extract b i :: r
         r.reverse
       else if s.get i == sep.get j then
         let i := s.next i
         let j := sep.next j
         if sep.atEnd j then
-          loop i i 0 ({ str := str, startPos := b, stopPos := i-j } :: r)
+          loop i i 0 (s.extract b (i-j) :: r)
         else
           loop b i j r
       else
         loop b (s.next i) 0 r
-    loop s.startPos s.startPos 0 []
+    loop 0 0 0 []
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring) : α :=
   match s with
diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean
index de2049cb4b..98c1b58014 100644
--- a/tests/lean/string_imp2.lean
+++ b/tests/lean/string_imp2.lean
@@ -53,4 +53,9 @@ it₁.remainingToString ++ "-" ++ it₂.remainingToString
 def ss : Substring := "0123abcdαβγδ".toSubstring
 #eval ss.drop 4 |>.takeRight 4
 #eval ss.drop 4 |>.take 4
-#eval ss.dropRight 4 |>.takeRight 4
\ No newline at end of file
+#eval ss.dropRight 4 |>.takeRight 4
+
+def ssDots : Substring := "____abc.αβγ.123.____".toSubstring.extract 4 19
+#eval ssDots.splitOn "."
+def ssHyphs : Substring := "____abc--αβγ--123--____".toSubstring.extract 4 22
+#eval ssHyphs.splitOn "--"
diff --git a/tests/lean/string_imp2.lean.expected.out b/tests/lean/string_imp2.lean.expected.out
index 8e18242b9e..62307c85b9 100644
--- a/tests/lean/string_imp2.lean.expected.out
+++ b/tests/lean/string_imp2.lean.expected.out
@@ -40,3 +40,5 @@ false
 "αβγδ".toSubstring
 "abcd".toSubstring
 "abcd".toSubstring
+["abc".toSubstring, "αβγ".toSubstring, "123".toSubstring, "".toSubstring]
+["abc".toSubstring, "αβγ".toSubstring, "123".toSubstring, "".toSubstring]