From ca0b11137aae60cdf565abdb12409e014edff84f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Oct 2020 09:29:10 -0700
Subject: [PATCH] chore: add `ShareCommonM.run`, and remove workaround

---
 src/Lean/Elab/PreDefinition/Basic.lean | 2 +-
 src/Std/ShareCommon.lean               | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 518e00123b..579a614341 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -61,7 +61,7 @@ private def shareCommon (preDefs : Array PreDefinition) : Array PreDefinition :=
 let result : Std.ShareCommonM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
     pure { preDef with type := (← Std.withShareCommon preDef.type), value := (← Std.withShareCommon preDef.value) }
-result.run (m := Id) -- TODO: remove (m := Id)
+result.run
 
 def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do
 let preDefs := shareCommon preDefs
diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean
index e4e1a6b423..e2ea4fc299 100644
--- a/src/Std/ShareCommon.lean
+++ b/src/Std/ShareCommon.lean
@@ -143,6 +143,12 @@ x.run' ShareCommon.State.empty
 @[inline] def PShareCommonT.run {m : Type u → Type v} [Monad m] {α : Type u} (x : PShareCommonT m α) : m α :=
 x.run' ShareCommon.PersistentState.empty
 
+@[inline] def ShareCommonM.run {α : Type u} (x : ShareCommonM α) : α :=
+Id.run x.run
+
+@[inline] def PShareCommonM.run {α : Type u} (x : PShareCommonM α) : α :=
+Id.run x.run
+
 def shareCommon {α} (a : α) : α :=
 (withShareCommon a : ShareCommonM α).run