diff --git a/cryptol.cabal b/cryptol.cabal
index d438734c..ceb23e38 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -138,7 +138,6 @@ library
                        Cryptol.Testing.Random,
 
                        Cryptol.Symbolic,
-                       Cryptol.Symbolic.BitVector,
                        Cryptol.Symbolic.Prims,
                        Cryptol.Symbolic.Value,
 
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
index 02692caf..fd45ce96 100644
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -27,7 +27,6 @@ import qualified Data.SBV.Dynamic as SBV
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.Env as M
 
-import Cryptol.Symbolic.BitVector
 import Cryptol.Symbolic.Prims
 import Cryptol.Symbolic.Value
 
diff --git a/src/Cryptol/Symbolic/BitVector.hs b/src/Cryptol/Symbolic/BitVector.hs
deleted file mode 100644
index 3c79c410..00000000
--- a/src/Cryptol/Symbolic/BitVector.hs
+++ /dev/null
@@ -1,48 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2013-2015 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
-
-{-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE ViewPatterns #-}
-
-module Cryptol.Symbolic.BitVector
-  ( SBool, SWord
-  , literalSWord
-  , fromBitsLE
-  , forallBV_, existsBV_
-  , forallSBool_, existsSBool_
-  ) where
-
-import Data.List (foldl')
-
-import Data.SBV.Dynamic
-
-type SBool = SVal
-type SWord = SVal
-
-fromBitsLE :: [SVal] -> SWord
-fromBitsLE bs = foldl' f (literalSWord 0 0) bs
-  where f w b = svJoin (svToWord1 b) w
-
-literalSWord :: Int -> Integer -> SWord
-literalSWord w i = svInteger (KBounded False w) i
-
-forallBV_ :: Int -> Symbolic SWord
-forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing
-
-existsBV_ :: Int -> Symbolic SWord
-existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing
-
-forallSBool_ :: Symbolic SBool
-forallSBool_ = svMkSymVar (Just ALL) KBool Nothing
-
-existsSBool_ :: Symbolic SBool
-existsSBool_ = svMkSymVar (Just EX) KBool Nothing
diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs
index cb3324c4..c97455d0 100644
--- a/src/Cryptol/Symbolic/Prims.hs
+++ b/src/Cryptol/Symbolic/Prims.hs
@@ -18,7 +18,6 @@ import Data.Ord (comparing)
 import Cryptol.Eval.Value (BitWord(..))
 import Cryptol.Prims.Eval (binary, unary, tlamN)
 import Cryptol.Prims.Syntax (ECon(..))
-import Cryptol.Symbolic.BitVector
 import Cryptol.Symbolic.Value
 import Cryptol.TypeCheck.AST (Name)
 import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs
index c15fac52..482de667 100644
--- a/src/Cryptol/Symbolic/Value.hs
+++ b/src/Cryptol/Symbolic/Value.hs
@@ -12,7 +12,12 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Cryptol.Symbolic.Value
-  ( Value
+  ( SBool, SWord
+  , literalSWord
+  , fromBitsLE
+  , forallBV_, existsBV_
+  , forallSBool_, existsSBool_
+  , Value
   , TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
   , GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
   , fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
@@ -22,14 +27,41 @@ module Cryptol.Symbolic.Value
   )
   where
 
-import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq,
-                           GenValue(..), BitWord(..), lam, tlam, toStream, toFinSeq, toSeq, fromSeq,
-                           fromVBit, fromVWord, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord)
-import Cryptol.Symbolic.BitVector
-import Cryptol.Utils.Panic (panic)
+import Data.List (foldl')
 
 import Data.SBV.Dynamic
 
+import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,
+                           isTFun, isTSeq, isTTuple, isTRec, tvSeq, GenValue(..),
+                           BitWord(..), lam, tlam, toStream, toFinSeq, toSeq,
+                           fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
+                           fromVTuple, fromVRecord, lookupRecord)
+import Cryptol.Utils.Panic (panic)
+
+-- SBool and SWord -------------------------------------------------------------
+
+type SBool = SVal
+type SWord = SVal
+
+fromBitsLE :: [SBool] -> SWord
+fromBitsLE bs = foldl' f (literalSWord 0 0) bs
+  where f w b = svJoin (svToWord1 b) w
+
+literalSWord :: Int -> Integer -> SWord
+literalSWord w i = svInteger (KBounded False w) i
+
+forallBV_ :: Int -> Symbolic SWord
+forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing
+
+existsBV_ :: Int -> Symbolic SWord
+existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing
+
+forallSBool_ :: Symbolic SBool
+forallSBool_ = svMkSymVar (Just ALL) KBool Nothing
+
+existsSBool_ :: Symbolic SBool
+existsSBool_ = svMkSymVar (Just EX) KBool Nothing
+
 -- Values ----------------------------------------------------------------------
 
 type Value = GenValue SBool SWord