diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index b1ff44e389..d8b34a56f1 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -97,7 +97,7 @@ def toList (m : SMap α β) : List (α × β) :=
 
 end SMap
 
-def List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
+def _root_.List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
   es.foldl (init := {}) fun s (a, b) => s.insert a b
 
 instance {_ : BEq α} {_ : Hashable α} [Repr α] [Repr β] : Repr (SMap α β) where