diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 950cbe45c8..8a14fd58ef 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -455,7 +455,7 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
   modify fun s => { s with scopes := s.scopes.drop ns.getNumParts }
   pure a
 
-@[specialize] def modifyScope (f : Scope → Scope) : CommandElabM Unit :=
+def modifyScope (f : Scope → Scope) : CommandElabM Unit :=
   modify fun s => { s with
     scopes := match s.scopes with
       | h::t => f h :: t
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index f690b69a4e..facef30ffa 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -232,7 +232,7 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData :=
 
 /- Return true if the give code contains an exit point that satisfies `p` -/
 @[inline] partial def hasExitPointPred (c : Code) (p : Code → Bool) : Bool :=
-  let rec @[specialize] loop : Code → Bool
+  let rec loop : Code → Bool
     | Code.decl _ _ k           => loop k
     | Code.reassign _ _ k       => loop k
     | Code.joinpoint _ _ b k    => loop b || loop k
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 4d4280021a..9348efb0b0 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -422,7 +422,7 @@ private def mkSubstructSource (structName : Name) (fieldNames : Array Name) (fie
     return Source.explicit stx (mkProj structName idx src)
   | s => return s
 
-@[specialize] private def groupFields (expandStruct : Struct → TermElabM Struct) (s : Struct) : TermElabM Struct := do
+private def groupFields (expandStruct : Struct → TermElabM Struct) (s : Struct) : TermElabM Struct := do
   let env ← getEnv
   let fieldNames := getStructureFields env s.structName
   withRef s.ref do
@@ -455,7 +455,7 @@ def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
     | [FieldLHS.fieldName _ n] => n == fieldName
     | _                        => false
 
-@[specialize] private def addMissingFields (expandStruct : Struct → TermElabM Struct) (s : Struct) : TermElabM Struct := do
+private def addMissingFields (expandStruct : Struct → TermElabM Struct) (s : Struct) : TermElabM Struct := do
   let env ← getEnv
   let fieldNames := getStructureFields env s.structName
   let ref := s.ref