diff --git a/src/Init.lean b/src/Init.lean
index 40d6ec9df0..8d425ad15e 100644
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -13,4 +13,3 @@ import Init.System
 import Init.Util
 import Init.Fix
 import Init.LeanInit
-import Init.ShareCommon
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 7ca3378e88..bb4f33ddb0 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-
+import Init.Data.HashSet -- TODO
 namespace Lean
 
 instance stringToName : HasCoe String Name :=
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index a6a731fbe6..52a9110be1 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Init.Data.PersistentHashMap
 universes u v w w'
 
 namespace Lean
diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean
index abf9717c40..33b96724dc 100644
--- a/src/Lean/Elab/Definition.lean
+++ b/src/Lean/Elab/Definition.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
+import Std.ShareCommon
 import Lean.Util.CollectLevelParams
 import Lean.Util.FoldConsts
 import Lean.Util.CollectFVars
@@ -99,9 +100,9 @@ else withUsedWhen ref vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun var
   val  ← Term.levelMVarToParam val;
   type ← Term.instantiateMVars ref type;
   val  ← Term.instantiateMVars view.val val;
-  let shareCommonTypeVal : ShareCommonM (Expr × Expr) := do {
-    type ← withShareCommon type;
-    val  ← withShareCommon val;
+  let shareCommonTypeVal : Std.ShareCommonM (Expr × Expr) := do {
+    type ← Std.withShareCommon type;
+    val  ← Std.withShareCommon val;
     pure (type, val)
   };
   let (type, val) := shareCommonTypeVal.run;
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index d4df1bd956..52c4f91c8f 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Init.Data.PersistentHashMap -- TODO
+import Init.Data.PersistentHashSet -- TODO
 import Lean.Data.Name
 import Lean.Data.Format
 
diff --git a/src/Lean/Util/Closure.lean b/src/Lean/Util/Closure.lean
index 854f6299d6..9fc003aa2c 100644
--- a/src/Lean/Util/Closure.lean
+++ b/src/Lean/Util/Closure.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Std.ShareCommon
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Util.FoldConsts
@@ -148,9 +149,9 @@ structure MkClosureResult :=
 (exprClosure  : Array Expr)
 
 def mkClosure (mctx : MetavarContext) (lctx : LocalContext) (type : Expr) (value : Expr) : Except String MkClosureResult :=
-let shareCommonTypeValue : ShareCommonM (Expr × Expr) := do {
-  type  ← withShareCommon type;
-  value ← withShareCommon value;
+let shareCommonTypeValue : Std.ShareCommonM (Expr × Expr) := do {
+  type  ← Std.withShareCommon type;
+  value ← Std.withShareCommon value;
   pure (type, value)
 };
 let (type, value) := shareCommonTypeValue.run;
diff --git a/src/Std.lean b/src/Std.lean
index 350c0228e1..50010f266c 100644
--- a/src/Std.lean
+++ b/src/Std.lean
@@ -4,3 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Std.Data
+import Std.ShareCommon
diff --git a/src/Init/ShareCommon.lean b/src/Std/ShareCommon.lean
similarity index 98%
rename from src/Init/ShareCommon.lean
rename to src/Std/ShareCommon.lean
index faca73ca5e..168a9b9b11 100644
--- a/src/Init/ShareCommon.lean
+++ b/src/Std/ShareCommon.lean
@@ -3,14 +3,10 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-prelude
-import Init.Util
-import Init.Data.HashMap
 import Init.Data.HashSet
-import Init.Data.PersistentHashSet
 import Init.Data.PersistentHashMap
-import Init.Control.State
-
+import Init.Data.PersistentHashSet
+namespace Std
 universes u v
 
 namespace ShareCommon
@@ -118,7 +114,7 @@ end ShareCommon
 class MonadShareCommon (m : Type u → Type v) :=
 (withShareCommon {α : Type u} : α → m α)
 
-export MonadShareCommon (withShareCommon)
+abbrev withShareCommon := @MonadShareCommon.withShareCommon
 
 abbrev shareCommonM {α : Type u} {m : Type u → Type v} [MonadShareCommon m] (a : α) : m α :=
 withShareCommon a
@@ -148,3 +144,5 @@ x.run' ShareCommon.PersistentState.empty
 
 def shareCommon {α} (a : α) : α :=
 (withShareCommon a : ShareCommonM α).run
+
+end Std