diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index bb36ff76dd..d5b8f9025c 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/src/Init/Lean/Elab/Definition.lean
@@ -98,6 +98,7 @@ else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
   val  ← Term.levelMVarToParam val;
   type ← Term.instantiateMVars ref type;
   val  ← Term.instantiateMVars view.val val;
+  Term.trace `Elab.definition.body ref $ fun _ => val;
   let usedParams : CollectLevelParams.State := {};
   let usedParams  := collectLevelParams usedParams type;
   let usedParams  := collectLevelParams usedParams val;
@@ -153,6 +154,10 @@ withDeclId view.declId $ fun name => do
     compileDecl ref decl;
     applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
 
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Elab.definition;
+pure ()
+
 end Command
 end Elab
 end Lean