diff --git a/src/Data/String.agda b/src/Data/String.agda
index fffe1ac300..70ebc2d2d6 100644
--- a/src/Data/String.agda
+++ b/src/Data/String.agda
@@ -9,27 +9,14 @@
 module Data.String where
 
 open import Data.Bool using (true; false; T?)
-open import Data.Char as Char using (Char)
 open import Function.Base
 open import Data.Nat.Base as ℕ using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉)
 import Data.Nat.Properties as ℕₚ
 open import Data.List.Base as List using (List; _∷_; []; [_])
 open import Data.List.NonEmpty as NE using (List⁺)
 open import Data.List.Extrema ℕₚ.≤-totalOrder
-open import Data.List.Relation.Binary.Pointwise using (Pointwise)
-open import Data.List.Relation.Binary.Lex.Strict using (Lex-<; Lex-≤)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Char.Base as Char using (Char)
-import Data.Char.Properties as Char using (_≟_)
-open import Function
-open import Relation.Binary using (Rel)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Relation.Nullary.Decidable using (does)
-open import Relation.Unary using (Pred; Decidable)
-
-open import Data.List.Membership.DecPropositional Char._≟_
-
-
 
 ------------------------------------------------------------------------
 -- Re-export contents of base, and decidability of equality
@@ -46,14 +33,6 @@ toVec s = Vec.fromList (toList s)
 fromVec : ∀ {n} → Vec Char n → String
 fromVec = fromList ∘ Vec.toList
 
-
--- enclose string with parens if it contains a space character
-parensIfSpace : String → String
-parensIfSpace s with does (' ' ∈? toList s)
-... | true  = parens s
-... | false = s
-
-
 ------------------------------------------------------------------------
 -- Rectangle
 
@@ -76,5 +55,6 @@ rectangleˡ c = rectangle (Vec.replicate $ padLeft c)
 rectangleʳ : ∀ {n} → Char → Vec String n → Vec String n
 rectangleʳ c = rectangle (Vec.replicate $ padRight c)
 
+
 rectangleᶜ : ∀ {n} → Char → Char → Vec String n → Vec String n
 rectangleᶜ cₗ cᵣ = rectangle (Vec.replicate $ padBoth cₗ cᵣ)
diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda
index 1a56376f59..7e7e293e01 100644
--- a/src/Data/String/Base.agda
+++ b/src/Data/String/Base.agda
@@ -8,9 +8,12 @@
 
 module Data.String.Base where
 
+
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Char.Base as Char using (Char)
+import Data.Char.Properties as Char
 open import Data.List.Base as List using (List; [_]; _∷_; [])
+import Data.List.Membership.DecSetoid as Membership
 open import Data.List.NonEmpty.Base as NE using (List⁺)
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
 open import Data.List.Relation.Binary.Lex.Core using (Lex-<; Lex-≤)
@@ -21,9 +24,12 @@ open import Function.Base using (_on_; _∘′_; _∘_)
 open import Level using (Level; 0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable.Core using (does)
 
+open Membership (decSetoid Char._≟_) using (_∈?_)
+
 ------------------------------------------------------------------------
 -- From Agda.Builtin: type and renamed primitives
 
@@ -115,6 +121,12 @@ _<+>_ : String → String → String
 a <+> "" = a
 a <+> b = a ++ " " ++ b
 
+-- enclose string with parens if it contains a space character
+parensIfSpace : String → String
+parensIfSpace s with does (' ' ∈? toList s)
+... | true  = parens s
+... | false = s
+
 ------------------------------------------------------------------------
 -- Padding