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

)
opencompl · Sep 18, 2024 · fa6afa8 · fa6afa8
1 parent 592e1dc
commit fa6afa8
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean
@@ -5,19 +5,18 @@ 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
 
 open ShareCommon
 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 :=