refactor: remove the last use of Lean.(HashSet|HashMap)

leanprover · Sep 16, 2024 · a3fb005 · a3fb005
1 parent 5eea835
commit a3fb005
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean
@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.ShareCommon
-import Lean.Data.HashSet
-import Lean.Data.HashMap
+import Std.Data.HashSet
+import Std.Data.HashMap
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 
@@ -16,8 +16,8 @@ namespace Lean.ShareCommon
 set_option linter.deprecated false in
 def objectFactory :=
   StateFactory.mk {
-    Map := HashMap, mkMap := (mkHashMap ·), mapFind? := (·.find?), mapInsert := (·.insert)
-    Set := HashSet, mkSet := (mkHashSet ·), setFind? := (·.find?), setInsert := (·.insert)
+    Map := Std.HashMap, mkMap := (Std.HashMap.empty ·), mapFind? := (·.get?), mapInsert := (·.insert)
+    Set := Std.HashSet, mkSet := (Std.HashSet.empty ·), setFind? := (·.get?), setInsert := (·.insert)
   }
 
 def persistentObjectFactory :=