diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index edc2222b7d..86e1c56c88 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -14,7 +14,7 @@ import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 open TSyntax.Compat
-open Simp (OriginSet)
+open Simp (UsedSimps)
 
 declare_config_elab elabSimpConfigCore    Meta.Simp.Config
 declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
@@ -249,7 +249,7 @@ register_builtin_option tactic.simp.trace : Bool := {
   descr    := "When tracing is enabled, calls to `simp` or `dsimp` will print an equivalent `simp only` call."
 }
 
-def traceSimpCall (stx : Syntax) (usedSimps : OriginSet) : MetaM Unit := do
+def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
   let mut stx := stx
   if stx[3].isNone then
     stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
@@ -257,7 +257,7 @@ def traceSimpCall (stx : Syntax) (usedSimps : OriginSet) : MetaM Unit := do
   let mut localsOrStar := some #[]
   let lctx ← getLCtx
   let env ← getEnv
-  for thm in usedSimps do
+  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
     | .decl declName => -- global definitions in the environment
       if env.contains declName && !simpOnlyBuiltins.contains declName then
@@ -298,7 +298,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM OriginSet := do
+def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -308,7 +308,7 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM OriginSet := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
     let mvarId ← getMainGoal
     let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 3a7e5b40c1..3aa63363d1 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -690,7 +690,7 @@ where
       modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
     return r
 
-def main (e : Expr) (ctx : Context) (usedSimps : OriginSet := {}) (methods : Methods := {}) : MetaM (Result × OriginSet) := do
+def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
   let ctx := { ctx with config := (← ctx.config.updateArith) }
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
     try
@@ -699,7 +699,7 @@ def main (e : Expr) (ctx : Context) (usedSimps : OriginSet := {}) (methods : Met
     catch ex =>
       if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex
 
-def dsimpMain (e : Expr) (ctx : Context) (usedSimps : OriginSet := {}) (methods : Methods := {}) : MetaM (Expr × OriginSet) := do
+def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
     try
       let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
@@ -810,16 +810,16 @@ def methods : Methods :=
 end DefaultMethods
 
 end Simp
-open Simp (OriginSet)
+open Simp (UsedSimps)
 
 def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : OriginSet := {}) : MetaM (Simp.Result × OriginSet) := do profileitM Exception "simp" (← getOptions) do
+    (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
   | none   => Simp.main e ctx usedSimps (methods := Simp.DefaultMethods.methods)
   | some d => Simp.main e ctx usedSimps (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d })
 
 def dsimp (e : Expr) (ctx : Simp.Context)
-    (usedSimps : OriginSet := {}) : MetaM (Expr × OriginSet) := do profileitM Exception "dsimp" (← getOptions) do
+    (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
   Simp.dsimpMain e ctx usedSimps (methods := Simp.DefaultMethods.methods)
 
 /--
@@ -837,7 +837,7 @@ def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result)
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option MVarId × OriginSet) := do
+    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   let target ← instantiateMVars (← mvarId.getType)
   let (r, usedSimps) ← simp target ctx discharge? usedSimps
   if mayCloseGoal && r.expr.isConstOf ``True then
@@ -852,7 +852,7 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
 def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option MVarId × OriginSet) :=
+    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     simpTargetCore mvarId ctx discharge? mayCloseGoal usedSimps
@@ -887,7 +887,7 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option (Expr × Expr) × OriginSet) := do
+    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
   let (r, usedSimps) ← simp prop ctx discharge? usedSimps
   return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
 
@@ -920,7 +920,7 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
     applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
 def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : OriginSet := {}) : MetaM (Option (FVarId × MVarId) × OriginSet) := do
+    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let type ← instantiateMVars (← fvarId.getType)
@@ -929,7 +929,7 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (disc
 
 def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : OriginSet := {}) : MetaM (Option (Array FVarId × MVarId) × OriginSet) := do
+    (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarId := mvarId
@@ -964,7 +964,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
     return (some (fvarIdsNew, mvarIdNew), usedSimps)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : OriginSet := {}) : MetaM (TacticResultCNM × OriginSet) := mvarId.withContext do
+    (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
@@ -980,11 +980,11 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S
       return (TacticResultCNM.modified mvarId', usedSimps')
 
 def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : OriginSet := {}) : MetaM (Option MVarId × OriginSet) := do
+    (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarId := mvarId
-    let mut usedSimps : OriginSet := usedSimps
+    let mut usedSimps : UsedSimps := usedSimps
     for fvarId in fvarIdsToSimp do
       let type ← instantiateMVars (← fvarId.getType)
       let (typeNew, usedSimps') ← dsimp type ctx
diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
index 5f9ec57b5f..2b91db680c 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-open Simp (OriginSet)
+open Simp (UsedSimps)
 
 namespace SimpAll
 
@@ -26,7 +26,7 @@ structure State where
   mvarId    : MVarId
   entries   : Array Entry := #[]
   ctx       : Simp.Context
-  usedSimps : OriginSet := {}
+  usedSimps : UsedSimps := {}
 
 abbrev M := StateRefT State MetaM
 
@@ -126,7 +126,7 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : OriginSet := {}) : MetaM (Option MVarId × OriginSet) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   mvarId.withContext do
     let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps }
     return (r, s.usedSimps)
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index dc7dc0d2b8..2620e6e54a 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -35,12 +35,12 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
 def Context.mkDefault : MetaM Context :=
   return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) }
 
-abbrev OriginSet := Std.HashSet Origin
+abbrev UsedSimps := Std.HashMap Origin Nat
 
 structure State where
   cache        : Cache := {}
   congrCache   : CongrCache := {}
-  usedTheorems : OriginSet := {}
+  usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
 
 abbrev SimpM := ReaderT Context $ StateRefT State MetaM
@@ -101,7 +101,9 @@ def getSimpCongrTheorems : M SimpCongrTheorems :=
     modify fun s => { s with cache := cacheSaved }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
-  modify fun s => { s with usedTheorems := s.usedTheorems.insert thmId }
+  modify fun s => if s.usedTheorems.contains thmId then s else
+    let n := s.usedTheorems.size
+    { s with usedTheorems := s.usedTheorems.insert thmId n }
 
 end Simp