diff --git a/tests/playground/deriving.lean b/tests/playground/deriving.lean
index a40271ad5d..1b32a8971f 100644
--- a/tests/playground/deriving.lean
+++ b/tests/playground/deriving.lean
@@ -99,14 +99,6 @@ namespace Deriving
 /- For type classes such as BEq, ToString, Format -/
 namespace Default
 
-structure AuxFun where
-  name    : Name
-  declSig : Array Syntax := #[]
-  type    : Syntax       := Syntax.missing
-  value   : Syntax       := Syntax.missing
-
-structure State where
-  auxFns  : NameMap AuxFun -- type name to function
 
 structure ContextCore where
   classInfo   : ConstantInfo