diff --git a/src/Lean/Meta/Sym/Simp/Theorems.lean b/src/Lean/Meta/Sym/Simp/Theorems.lean
index b57430f952..5207558b76 100644
--- a/src/Lean/Meta/Sym/Simp/Theorems.lean
+++ b/src/Lean/Meta/Sym/Simp/Theorems.lean
@@ -24,6 +24,7 @@ structure Theorem where
   pattern : Pattern
   /-- Right-hand side of the equation. -/
   rhs     : Expr
+  deriving Inhabited
 
 instance : BEq Theorem where
   beq thm₁ thm₂ := thm₁.expr == thm₂.expr