diff --git a/Data/Logic/Classes/Equals.hs b/Data/Logic/Classes/Equals.hs
--- a/Data/Logic/Classes/Equals.hs
+++ b/Data/Logic/Classes/Equals.hs
@@ -49,7 +49,7 @@
 -- | A way to represent any predicate's name.  Frequently the equality
 -- predicate has no standalone representation in the p type, it is
 -- just a constructor in the atom type, or even the formula type.
-data Ord p => PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show)
+data PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show)
 
 instance (Pretty p, Ord p) => Pretty (PredicateName p) where
     pretty Equals = text "="
diff --git a/Data/Logic/Instances/SatSolver.hs b/Data/Logic/Instances/SatSolver.hs
--- a/Data/Logic/Instances/SatSolver.hs
+++ b/Data/Logic/Instances/SatSolver.hs
@@ -4,7 +4,7 @@
 
 import Control.Monad.State (get, put)
 import Control.Monad.Trans (lift)
-import Data.Boolean.SatSolver
+import Data.Boolean.SatSolver (Literal(Pos, Neg), CNF, newSatSolver, assertTrue', solve)
 import Data.Generics (Data, Typeable)
 import qualified Data.Set.Extra as S
 import Data.Logic.Classes.Atom (Atom)
diff --git a/Data/Logic/Normal/Implicative.hs b/Data/Logic/Normal/Implicative.hs
--- a/Data/Logic/Normal/Implicative.hs
+++ b/Data/Logic/Normal/Implicative.hs
@@ -52,7 +52,7 @@
 -- formula has the form @a & b & c .=>. d | e | f@, where a thru f are
 -- literals.  One more restriction that is not implied by the type is
 -- that no literal can appear in both the pos set and the neg set.
-data (Negatable lit, Ord lit) => ImplicativeForm lit =
+data ImplicativeForm lit =
     INF {neg :: Set.Set lit, pos :: Set.Set lit}
     deriving (Eq, Ord, Data, Typeable, Show)
 
diff --git a/logic-classes.cabal b/logic-classes.cabal
--- a/logic-classes.cabal
+++ b/logic-classes.cabal
@@ -1,5 +1,5 @@
 Name:             logic-classes
-Version:          1.4.5
+Version:          1.4.6
 Synopsis:         Framework for propositional and first order logic, theorem proving
 Description:      Package to support Propositional and First Order Logic.  It includes classes
                   representing the different types of formulas and terms, some instances of