diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean
index d8ee0b4a51..c95f37a989 100644
--- a/src/Init/Control/ExceptCps.lean
+++ b/src/Init/Control/ExceptCps.lean
@@ -29,7 +29,7 @@ instance : Monad (ExceptCpsT ε m) where
   bind x f := fun _ k₁ k₂ => x _ (fun a => f a _ k₁ k₂) k₂
 
 instance : LawfulMonad (ExceptCpsT σ m) := by
-  refine! { .. } <;> intros <;> rfl
+  refine' { .. } <;> intros <;> rfl
 
 instance : MonadExceptOf ε (ExceptCpsT ε m) where
   throw e  := fun _ _ k => k e
diff --git a/src/Init/Control/Lawful.lean b/src/Init/Control/Lawful.lean
index 7ab038e53b..d400331b7e 100644
--- a/src/Init/Control/Lawful.lean
+++ b/src/Init/Control/Lawful.lean
@@ -102,7 +102,7 @@ namespace Id
 @[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
 
 instance : LawfulMonad Id := by
-  refine! { .. } <;> intros <;> rfl
+  refine' { .. } <;> intros <;> rfl
 
 end Id
 
diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean
index 6b00d4030e..6a1c39c835 100644
--- a/src/Init/Control/StateCps.lean
+++ b/src/Init/Control/StateCps.lean
@@ -29,7 +29,7 @@ instance : Monad (StateCpsT σ m) where
   bind x f := fun δ s k => x δ s fun a s => f a δ s k
 
 instance : LawfulMonad (StateCpsT σ m) := by
-  refine! { .. } <;> intros <;> rfl
+  refine' { .. } <;> intros <;> rfl
 
 instance : MonadStateOf σ (StateCpsT σ m) where
   get   := fun δ s k => k s s
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 485bb4e86d..e52b0c42db 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -28,7 +28,6 @@ macro "min1" : prec => `(11)   -- `(min+1) we can only `min+1` after `Meta.lean`
 /-
   `max:prec` as a term. It is equivalent to `eval_prec max` for `eval_prec` defined at `Meta.lean`.
   We use `max_prec` to workaround bootstrapping issues. -/
-macro "maxPrec!" : term => `(1024)
 macro "max_prec" : term => `(1024)
 
 macro "default" : prio => `(1000)
@@ -198,7 +197,6 @@ syntax (name := contradiction) "contradiction" : tactic
 syntax (name := apply) "apply " term : tactic
 syntax (name := exact) "exact " term : tactic
 syntax (name := refine) "refine " term : tactic
-syntax (name := refine!) "refine! " term : tactic
 syntax (name := refine') "refine' " term : tactic
 syntax (name := case) "case " ident " => " tacticSeq : tactic
 syntax (name := allGoals) "allGoals " tacticSeq : tactic
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 3ea4575a8f..5be36211d9 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -73,11 +73,6 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
   | `(tactic| refine $e) => refineCore e `refine (allowNaturalHoles := false)
   | _                    => throwUnsupportedSyntax
 
-@[builtinTactic «refine!»] def evalRefineBang : Tactic := fun stx =>
-  match stx with
-  | `(tactic| refine! $e) => refineCore e `refine (allowNaturalHoles := true)
-  | _                     => throwUnsupportedSyntax
-
 @[builtinTactic «refine'»] def evalRefine' : Tactic := fun stx =>
   match stx with
   | `(tactic| refine' $e) => refineCore e `refine' (allowNaturalHoles := true)