diff --git a/src/Init/Lean/Meta/Tactic/Clear.lean b/src/Init/Lean/Meta/Tactic/Clear.lean
index fd9267f5f6..330caf0a6b 100644
--- a/src/Init/Lean/Meta/Tactic/Clear.lean
+++ b/src/Init/Lean/Meta/Tactic/Clear.lean
@@ -20,7 +20,7 @@ withMVarContext mvarId $ do
   lctx.forM $ fun localDecl =>
     unless (localDecl.fvarId == fvarId) $
       when (mctx.localDeclDependsOn localDecl fvarId) $
-        throwTacticEx `clear mvarId ("variable '" ++ localDecl.value ++ "' depends on '" ++ mkFVar fvarId ++ "'");
+        throwTacticEx `clear mvarId ("variable '" ++ localDecl.toExpr ++ "' depends on '" ++ mkFVar fvarId ++ "'");
   mvarDecl ← getMVarDecl mvarId;
   when (mctx.exprDependsOn mvarDecl.type fvarId) $
     throwTacticEx `clear mvarId ("taget depends on '" ++ mkFVar fvarId ++ "'");