diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean
index 4a250d9aac..003b118a74 100644
--- a/src/Lean/Util/Sorry.lean
+++ b/src/Lean/Util/Sorry.lean
@@ -5,72 +5,54 @@ Authors: Leonardo de Moura
 -/
 import Lean.Message
 import Lean.Exception
+import Lean.Util.FindExpr
 
 namespace Lean
 
 def Expr.isSorry : Expr → Bool
-  | Expr.app (Expr.app (Expr.const ``sorryAx _ _) _ _) _ _ => true
+  | app (app (.const ``sorryAx ..) ..) .. => true
   | _ => false
 
 def Expr.isSyntheticSorry : Expr → Bool
-  | Expr.app (Expr.app (Expr.const ``sorryAx _ _) _ _) (Expr.const ``Bool.true _ _) _ => true
+  | app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) _ => true
   | _ => false
 
 def Expr.isNonSyntheticSorry : Expr → Bool
-  | Expr.app (Expr.app (Expr.const ``sorryAx _ _) _ _) (Expr.const ``Bool.false _ _) _ => true
+  | app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) _ => true
   | _ => false
 
-def Expr.hasSorry : Expr → Bool
-  | Expr.const c _ _     => c == `sorryAx
-  | Expr.app f a _       => f.hasSorry || a.hasSorry
-  | Expr.letE _ t v b _  => t.hasSorry || v.hasSorry || b.hasSorry
-  | Expr.forallE _ d b _ => d.hasSorry || b.hasSorry
-  | Expr.lam _ d b _     => d.hasSorry || b.hasSorry
-  | Expr.mdata _ e _     => e.hasSorry
-  | Expr.proj _ _ e _    => e.hasSorry
-  | _                    => false
+def Expr.hasSorry (e : Expr) : Bool :=
+  Option.isSome <| e.find? (·.isConstOf ``sorryAx)
 
-def Expr.hasSyntheticSorry : Expr → Bool
-  | e@(Expr.app f a _)   => e.isSyntheticSorry  || f.hasSyntheticSorry || a.hasSyntheticSorry
-  | Expr.letE _ t v b _  => t.hasSyntheticSorry || v.hasSyntheticSorry || b.hasSyntheticSorry
-  | Expr.forallE _ d b _ => d.hasSyntheticSorry || b.hasSyntheticSorry
-  | Expr.lam _ d b _     => d.hasSyntheticSorry || b.hasSyntheticSorry
-  | Expr.mdata _ e _     => e.hasSyntheticSorry
-  | Expr.proj _ _ e _    => e.hasSyntheticSorry
-  | _                    => false
+def Expr.hasSyntheticSorry (e : Expr) : Bool :=
+  Option.isSome <| e.find? (·.isSyntheticSorry)
 
-def Expr.hasNonSyntheticSorry : Expr → Bool
-  | e@(Expr.app f a _)   => e.isNonSyntheticSorry  || f.hasNonSyntheticSorry || a.hasNonSyntheticSorry
-  | Expr.letE _ t v b _  => t.hasNonSyntheticSorry || v.hasNonSyntheticSorry || b.hasNonSyntheticSorry
-  | Expr.forallE _ d b _ => d.hasNonSyntheticSorry || b.hasNonSyntheticSorry
-  | Expr.lam _ d b _     => d.hasNonSyntheticSorry || b.hasNonSyntheticSorry
-  | Expr.mdata _ e _     => e.hasNonSyntheticSorry
-  | Expr.proj _ _ e _    => e.hasNonSyntheticSorry
-  | _                    => false
+def Expr.hasNonSyntheticSorry (e : Expr) : Bool :=
+  Option.isSome <| e.find? (·.isNonSyntheticSorry)
 
 partial def MessageData.hasSorry : MessageData → Bool
-  | MessageData.ofExpr e          => e.hasSorry
-  | MessageData.withContext _ msg => msg.hasSorry
-  | MessageData.nest _ msg        => msg.hasSorry
-  | MessageData.group msg         => msg.hasSorry
-  | MessageData.compose msg₁ msg₂ => msg₁.hasSorry || msg₂.hasSorry
-  | MessageData.tagged _ msg      => msg.hasSorry
-  | MessageData.node msgs         => msgs.any hasSorry
-  | _                             => false
+  | ofExpr e          => e.hasSorry
+  | withContext _ msg => msg.hasSorry
+  | nest _ msg        => msg.hasSorry
+  | group msg         => msg.hasSorry
+  | compose msg₁ msg₂ => msg₁.hasSorry || msg₂.hasSorry
+  | tagged _ msg      => msg.hasSorry
+  | node msgs         => msgs.any hasSorry
+  | _                 => false
 
 partial def MessageData.hasSyntheticSorry (msg : MessageData) : Bool :=
   visit msg.instantiateMVars
 where
   visit : MessageData → Bool
-  | MessageData.ofExpr e                => e.hasSyntheticSorry
-  | MessageData.withContext _ msg       => visit msg
-  | MessageData.withNamingContext _ msg => visit msg
-  | MessageData.nest _ msg              => visit msg
-  | MessageData.group msg               => visit msg
-  | MessageData.compose msg₁ msg₂       => visit msg₁ || visit msg₂
-  | MessageData.tagged _ msg            => visit msg
-  | MessageData.node msgs               => msgs.any hasSyntheticSorry
-  | _                                   => false
+  | ofExpr e                => e.hasSyntheticSorry
+  | withContext _ msg       => visit msg
+  | withNamingContext _ msg => visit msg
+  | nest _ msg              => visit msg
+  | group msg               => visit msg
+  | compose msg₁ msg₂       => visit msg₁ || visit msg₂
+  | tagged _ msg            => visit msg
+  | node msgs               => msgs.any hasSyntheticSorry
+  | _                       => false
 
 def Exception.hasSyntheticSorry : Exception → Bool
   | Exception.error _ msg => msg.hasSyntheticSorry