From 339a4cf7408e9449407f2fb7c8fca9698a753171 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Dec 2020 18:26:28 -0800
Subject: [PATCH] chore: remove `defaultInstance` for `ToString`

---
 src/Init/Data/ToString/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean
index 01b4335bd3..a70a3fbbdd 100644
--- a/src/Init/Data/ToString/Basic.lean
+++ b/src/Init/Data/ToString/Basic.lean
@@ -27,7 +27,6 @@ instance {α} [ToString α] : ToString (id α) :=
 instance {α} [ToString α] : ToString (Id α) :=
   inferInstanceAs (ToString α)
 
-@[defaultInstance low]
 instance : ToString String :=
   ⟨fun s => s⟩