diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean index 65b40dfb062b8..eef9fcafea3f6 100644 --- 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 :=