[ agda/agda#5000 ] removed spurious import

andreasabel · andreasabel · commit 811f21ddf432 · 2020-10-25T21:38:54.000+01:00
diff --git a/src/Codata/Thunk.agda b/src/Codata/Thunk.agda
@@ -8,7 +8,6 @@
 
 module Codata.Thunk where
 
-open import Level
 open import Size; open SizedType
 
 ------------------------------------------------------------------------
