From 892bfe2c5fdd964405d94f0adb0e178fe2b485af Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 8 Apr 2024 19:16:24 +0200
Subject: [PATCH] fix: remove unused trace.Elab.syntax option (#3844)

---
 src/Lean/Elab/Syntax.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index cacb920acc..40ad9430b3 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -442,7 +442,4 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax :=
   | some str => return mkAtomFrom stx str
   | none     => Macro.throwUnsupported
 
-builtin_initialize
-  registerTraceClass `Elab.syntax
-
 end Lean.Elab.Command