diff --git a/Data/Logic/Classes/Apply.hs b/Data/Logic/Classes/Apply.hs
--- a/Data/Logic/Classes/Apply.hs
+++ b/Data/Logic/Classes/Apply.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses,
+             RankNTypes, ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}
 {-# OPTIONS -fno-warn-missing-signatures #-}
 -- | The Apply class represents a type of atom the only supports predicate application.
 module Data.Logic.Classes.Apply
@@ -11,11 +12,13 @@
     , prettyApply
     , varApply
     , substApply
+    , pApp, pApp0, pApp1, pApp2, pApp3, pApp4, pApp5, pApp6, pApp7
     ) where
 
 import Data.Data (Data)
 import Data.Logic.Classes.Arity
 import Data.Logic.Classes.Constants
+import Data.Logic.Classes.Formula (Formula(atomic))
 import Data.Logic.Classes.Pretty (Pretty)
 import Data.Logic.Classes.Term (Term, showTerm, prettyTerm, fvt, tsubst)
 import Data.List (intercalate, intersperse)
@@ -62,7 +65,7 @@
               (\ x -> if x then "true" else "false")
 
 prettyApply :: (Apply atom p term, Term term v f) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> Int -> atom -> Doc
-prettyApply pv pp pf prec atom =
+prettyApply pv pp pf _prec atom =
     foldApply (\ p ts ->
                    pp p <> case ts of
                              [] -> empty
@@ -83,3 +86,24 @@
     freeVariables = varApply
     substitute = substApply
 -}
+
+pApp :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> [term] -> formula
+pApp p ts = atomic (apply p ts :: atom)
+
+-- | Versions of pApp specialized for different argument counts.
+pApp0 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> formula
+pApp0 p = atomic (apply0 p :: atom)
+pApp1 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> formula
+pApp1 p a = atomic (apply1 p a :: atom)
+pApp2 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> formula
+pApp2 p a b = atomic (apply2 p a b :: atom)
+pApp3 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> formula
+pApp3 p a b c = atomic (apply3 p a b c :: atom)
+pApp4 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> formula
+pApp4 p a b c d = atomic (apply4 p a b c d :: atom)
+pApp5 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula
+pApp5 p a b c d e = atomic (apply5 p a b c d e :: atom)
+pApp6 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
+pApp6 p a b c d e f = atomic (apply6 p a b c d e f :: atom)
+pApp7 :: forall formula atom term p. (Formula formula atom, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula
+pApp7 p a b c d e f g = atomic (apply7 p a b c d e f g :: atom)
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
@@ -34,7 +34,7 @@
 import Text.PrettyPrint (Doc, (<>), (<+>), text, empty, parens, hcat, nest)
 
 -- | Its not safe to make Atom a superclass of AtomEq, because the Atom methods will fail on AtomEq instances.
-class Predicate p => AtomEq atom p term | atom -> p term, term -> atom p where
+class Predicate p => AtomEq atom p term | atom -> term, atom -> p where
     foldAtomEq :: (p -> [term] -> r) -> (Bool -> r) -> (term -> term -> r) -> atom -> r
     equals :: term -> term -> atom
     applyEq' :: p -> [term] -> atom
@@ -110,7 +110,7 @@
 pApp7 :: (FirstOrderFormula formula atom v, AtomEq atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula
 pApp7 p a b c d e f g = atomic (apply7 p a b c d e f g)
 
-showFirstOrderFormulaEq :: (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String
+showFirstOrderFormulaEq :: forall fof atom v p term. (FirstOrderFormula fof atom v, AtomEq atom p term, Show term, Show v, Show p) => fof -> String
 showFirstOrderFormulaEq fm =
     fst (sfo fm)
     where
diff --git a/Data/Logic/Classes/FirstOrder.hs b/Data/Logic/Classes/FirstOrder.hs
--- a/Data/Logic/Classes/FirstOrder.hs
+++ b/Data/Logic/Classes/FirstOrder.hs
@@ -4,15 +4,6 @@
     ( FirstOrderFormula(..)
     , Quant(..)
     , zipFirstOrder
-    , pApp
-    , pApp0
-    , pApp1
-    , pApp2
-    , pApp3
-    , pApp4
-    , pApp5
-    , pApp6
-    , pApp7
     , for_all'
     , exists'
     , quant
@@ -37,7 +28,6 @@
     ) where
 
 import Data.Generics (Data, Typeable)
-import Data.Logic.Classes.Apply (Apply(..), apply, apply0, apply1, apply2, apply3, apply4, apply5, apply6, apply7)
 import Data.Logic.Classes.Constants
 import Data.Logic.Classes.Combine
 import Data.Logic.Classes.Formula (Formula(atomic))
@@ -101,27 +91,6 @@
 -- class, but it would add additional complexity with unclear
 -- benefits.
 data Quant = Forall | Exists deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)
-
-pApp :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> [term] -> formula
-pApp p ts = atomic (apply p ts :: atom)
-
--- | Versions of pApp specialized for different argument counts.
-pApp0 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> formula
-pApp0 p = atomic (apply0 p :: atom)
-pApp1 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> formula
-pApp1 p a = atomic (apply1 p a :: atom)
-pApp2 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> formula
-pApp2 p a b = atomic (apply2 p a b :: atom)
-pApp3 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> formula
-pApp3 p a b c = atomic (apply3 p a b c :: atom)
-pApp4 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> formula
-pApp4 p a b c d = atomic (apply4 p a b c d :: atom)
-pApp5 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> formula
-pApp5 p a b c d e = atomic (apply5 p a b c d e :: atom)
-pApp6 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> formula
-pApp6 p a b c d e f = atomic (apply6 p a b c d e f :: atom)
-pApp7 :: forall formula atom term v p. (FirstOrderFormula formula atom v, Apply atom p term) => p -> term -> term -> term -> term -> term -> term -> term -> formula
-pApp7 p a b c d e f g = atomic (apply7 p a b c d e f g :: atom)
 
 -- |for_all with a list of variables, for backwards compatibility.
 for_all' :: FirstOrderFormula formula atom v => [v] -> formula -> formula
diff --git a/Data/Logic/Classes/Formula.hs b/Data/Logic/Classes/Formula.hs
--- a/Data/Logic/Classes/Formula.hs
+++ b/Data/Logic/Classes/Formula.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses #-}
 module Data.Logic.Classes.Formula
     ( Formula(atomic, foldAtoms, mapAtoms)
     ) where
 
-class Formula formula atom where
+class Formula formula atom | formula -> atom where
     atomic :: atom -> formula
     foldAtoms :: Formula formula atom => (r -> atom -> r) -> r -> formula -> r
     mapAtoms :: Formula formula atom => (atom -> formula) -> formula -> formula
diff --git a/Data/Logic/Classes/Literal.hs b/Data/Logic/Classes/Literal.hs
--- a/Data/Logic/Classes/Literal.hs
+++ b/Data/Logic/Classes/Literal.hs
@@ -8,13 +8,11 @@
     , foldAtomsLiteral
     ) where
 
-import Data.Logic.Classes.Combine (Combination(..))
 import Data.Logic.Classes.Constants
 import Data.Logic.Classes.Formula (Formula(atomic))
 import Data.Logic.Classes.Pretty (HasFixity(..), Fixity(..), FixityDirection(..))
 import qualified Data.Logic.Classes.Propositional as P
 import Data.Logic.Classes.Negate
-import Data.Logic.Failing (Failing(..))
 import Text.PrettyPrint (Doc, (<>), text, parens, nest)
 
 -- |Literals are the building blocks of the clause and implicative normal
diff --git a/Data/Logic/Harrison/DefCNF.hs b/Data/Logic/Harrison/DefCNF.hs
--- a/Data/Logic/Harrison/DefCNF.hs
+++ b/Data/Logic/Harrison/DefCNF.hs
@@ -89,8 +89,8 @@
   let (deflist {- :: [pf]-}) = Map.elems defs in
   Set.unions (simpcnf fm'' : map simpcnf deflist)
 
-defcnf1 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> pf
-defcnf1 fm = cnf (mk_defcnf maincnf fm :: Set.Set (Set.Set lit))
+defcnf1 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf
+defcnf1 _ _ fm = cnf (mk_defcnf maincnf fm :: Set.Set (Set.Set lit))
 
 
 -- ------------------------------------------------------------------------- 
@@ -134,8 +134,8 @@
 defcnfs :: (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> Set.Set (Set.Set lit)
 defcnfs fm = mk_defcnf andcnf fm
 
-defcnf2 :: forall pf lit atom.(PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> pf
-defcnf2 fm = cnf (defcnfs fm :: Set.Set (Set.Set lit))
+defcnf2 :: forall pf lit atom.(PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf
+defcnf2 _ _ fm = cnf (defcnfs fm :: Set.Set (Set.Set lit))
 
 -- ------------------------------------------------------------------------- 
 -- Examples.                                                                 
@@ -156,5 +156,5 @@
       co (BinOp p (:&:) q) = subcnf andcnf3 (.&.) p q trip
       co _ = maincnf trip
 
-defcnf3 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => pf -> pf
-defcnf3 fm = cnf (mk_defcnf andcnf3 fm :: Set.Set (Set.Set lit))
+defcnf3 :: forall pf lit atom. (PropositionalFormula pf atom, Literal lit atom, NumAtom atom, Ord lit) => lit -> atom -> pf -> pf
+defcnf3 _ _ fm = cnf (mk_defcnf andcnf3 fm :: Set.Set (Set.Set lit))
diff --git a/Data/Logic/Harrison/Herbrand.hs b/Data/Logic/Harrison/Herbrand.hs
--- a/Data/Logic/Harrison/Herbrand.hs
+++ b/Data/Logic/Harrison/Herbrand.hs
@@ -134,8 +134,8 @@
             Atom atom term v,
             IsString f,
             Ord pf) =>
-           (atom -> Set.Set (f, Int)) -> fof -> Failing Int
-gilmore fa fm =
+           pf -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int
+gilmore _ fa fm =
   let sfm = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf in
   let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union s (freeVariables a)) Set.empty sfm)
       (consts,funcs) = herbfuns fa sfm in
@@ -224,8 +224,8 @@
                 Atom atom term v,
                 IsString f,
                 Ord lit) =>
-               (atom -> Set.Set (f, Int)) -> fof -> Failing Int
-davisputnam fa fm =
+               lit -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int
+davisputnam _ fa fm =
   let (sfm :: lit) = runSkolem (skolemize id ((.~.)(generalize fm))) in
   let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union (freeVariables a) s) Set.empty sfm)
       (consts,funcs) = herbfuns fa sfm in
@@ -284,8 +284,8 @@
                  Term term v f,
                  Atom atom term v,
                  IsString f) =>
-                (atom -> Set.Set (f, Int)) -> fof -> Failing Int
-davisputnam' fa fm =
+                lit -> pf -> (atom -> Set.Set (f, Int)) -> fof -> Failing Int
+davisputnam' _ _ fa fm =
     let (sfm :: pf) = runSkolem (skolemize id ((.~.)(generalize fm))) in
     let fvs = Set.toList (foldAtoms (\ s (a :: atom) -> Set.union (freeVariables a) s) Set.empty sfm)
         (consts,funcs) = herbfuns fa sfm in
diff --git a/Data/Logic/Harrison/Tableaux.hs b/Data/Logic/Harrison/Tableaux.hs
--- a/Data/Logic/Harrison/Tableaux.hs
+++ b/Data/Logic/Harrison/Tableaux.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE CPP, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables #-}
 {-# OPTIONS_GHC -Wall #-}
 module Data.Logic.Harrison.Tableaux
     ( unify_literals
@@ -112,6 +112,7 @@
       substitute' = C.substitute
 
 -- prawitz :: forall fof atom v. (FirstOrderFormula fof atom v, Ord fof) => fof -> Int
+#if 0
 prawitz :: forall fof atom term v f lit pf.
            (FirstOrderFormula fof atom v,
             PropositionalFormula pf atom,
@@ -126,6 +127,7 @@
       dnf = simpdnf pf :: Set.Set (Set.Set lit)
       fvs = foldAtoms (\ s (a :: atom) -> Set.union (C.freeVariables a) s) Set.empty pf :: Set.Set v
       pf = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf
+#endif
 
 -- ------------------------------------------------------------------------- 
 -- Examples.                                                                 
diff --git a/Data/Logic/Instances/Chiou.hs b/Data/Logic/Instances/Chiou.hs
deleted file mode 100644
--- a/Data/Logic/Instances/Chiou.hs
+++ /dev/null
@@ -1,307 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
-             RankNTypes, TypeSynonymInstances, UndecidableInstances #-}
-{-# OPTIONS -Wall -Wwarn -fno-warn-orphans -fno-warn-missing-signatures #-}
-module Data.Logic.Instances.Chiou
-    ( Sentence(..)
-    , CTerm(..)
-    , Connective(..)
-    , Quantifier(..)
-    , ConjunctiveNormalForm(..)
-    , NormalSentence(..)
-    , NormalTerm(..)
-    , toSentence
-    , fromSentence
-    ) where
-
-import Data.Generics (Data, Typeable)
-import Data.Logic.Classes.Apply (Apply(..), Predicate)
-import Data.Logic.Classes.Atom (Atom)
-import Data.Logic.Classes.Combine (Combinable(..), BinOp(..), Combination(..))
-import Data.Logic.Classes.Constants (Constants(..), asBool, true, false)
-import Data.Logic.Classes.Equals (AtomEq(..), (.=.))
-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), Quant(..), quant', pApp, prettyFirstOrder, fixityFirstOrder, foldAtomsFirstOrder, mapAtomsFirstOrder)
-import Data.Logic.Classes.Formula (Formula(..))
-import Data.Logic.Classes.Negate (Negatable(..), (.~.))
-import Data.Logic.Classes.Pretty (Pretty(pretty), HasFixity(..))
-import Data.Logic.Classes.Term (Term(..), Function)
-import Data.Logic.Classes.Variable (Variable)
-import qualified Data.Logic.Classes.FirstOrder as L
-import Data.Logic.Classes.Propositional (PropositionalFormula(..))
-import Data.Logic.Classes.Skolem (Skolem(..))
-import Data.String (IsString(..))
-
-data Sentence v p f
-    = Connective (Sentence v p f) Connective (Sentence v p f)
-    | Quantifier Quantifier [v] (Sentence v p f)
-    | Not (Sentence v p f)
-    | Predicate p [CTerm v f]
-    | Equal (CTerm v f) (CTerm v f)
-    deriving (Eq, Ord, Data, Typeable)
-
-data CTerm v f
-    = Function f [CTerm v f]
-    | Variable v
-    deriving (Eq, Ord, Data, Typeable)
-
-data Connective
-    = Imply
-    | Equiv
-    | And
-    | Or
-    deriving (Eq, Ord, Show, Data, Typeable)
-
-data Quantifier
-    = ForAll
-    | ExistsCh
-    deriving (Eq, Ord, Show, Data, Typeable)
-
-instance Negatable (Sentence v p f) where
-    negatePrivate = Not
-    foldNegation normal inverted (Not x) = foldNegation inverted normal x
-    foldNegation normal _ x = normal x
-
-instance (Constants p, Eq (Sentence v p f)) => Constants (Sentence v p f) where
-    fromBool x = Predicate (fromBool x) []
-    asBool x
-        | fromBool True == x = Just True
-        | fromBool False == x = Just False
-        | True = Nothing
-
-instance ({- Constants (Sentence v p f), -} Ord v, Ord p, Ord f) => Combinable (Sentence v p f) where
-    x .<=>. y = Connective x Equiv y
-    x .=>.  y = Connective x Imply y
-    x .|.   y = Connective x Or y
-    x .&.   y = Connective x And y
-
-instance (Predicate p, Function f v) => Formula (Sentence v p f) (Sentence v p f) where
-    atomic (Connective _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"
-    atomic (Quantifier _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"
-    atomic (Not _) = error "Logic.Instances.Chiou.atomic: unexpected"
-    atomic x@(Predicate _ _) = x
-    atomic x@(Equal _ _) = x
-    foldAtoms = foldAtomsFirstOrder
-    mapAtoms = mapAtomsFirstOrder
-
-instance (Formula (Sentence v p f) (Sentence v p f), Variable v, Predicate p, Function f v, Combinable (Sentence v p f)) =>
-         PropositionalFormula (Sentence v p f) (Sentence v p f) where
-    foldPropositional co tf at formula =
-        case formula of
-          Not x -> co ((:~:) x)
-          Quantifier _ _ _ -> error "Logic.Instance.Chiou.foldF0: unexpected"
-          Connective f1 Imply f2 -> co (BinOp f1 (:=>:) f2)
-          Connective f1 Equiv f2 -> co (BinOp f1 (:<=>:) f2)
-          Connective f1 And f2 -> co (BinOp f1 (:&:) f2)
-          Connective f1 Or f2 -> co (BinOp f1 (:|:) f2)
-          Predicate p ts -> maybe (at (Predicate p ts)) tf (asBool p)
-          Equal t1 t2 -> at (Equal t1 t2)
-
-data AtomicFunction v
-    = AtomicFunction String
-    -- This is redundant with the SkolemFunction and SkolemConstant
-    -- constructors in the Chiou Term type.
-    | AtomicSkolemFunction v
-    deriving (Eq, Show)
-
-instance IsString (AtomicFunction v) where
-    fromString = AtomicFunction
-
-instance Variable v => Skolem (AtomicFunction v) v where
-    toSkolem = AtomicSkolemFunction
-    isSkolem (AtomicSkolemFunction _) = True
-    isSkolem _ = False
-
--- The Atom type is not cleanly distinguished from the Sentence type, so we need an Atom instance for Sentence.
-instance (Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f) where
-    foldApply ap tf (Predicate p ts) = maybe (ap p ts) tf (asBool p)
-    foldApply _ _ _ = error "Data.Logic.Instances.Chiou: Invalid atom"
-    apply' = Predicate
-
-instance Predicate p => AtomEq (Sentence v p f) p (CTerm v f) where
-    foldAtomEq ap tf _ (Predicate p ts) = if p == true then tf True else if p == false then tf False else ap p ts
-    foldAtomEq _ _ eq (Equal t1 t2) = eq t1 t2
-    foldAtomEq _ _ _ _ = error "Data.Logic.Instances.Chiou: Invalid atom"
-    equals = Equal
-    applyEq' = Predicate
-
-instance (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Variable v, Predicate p, Function f v) => Pretty (Sentence v p f) where
-    pretty = prettyFirstOrder (\ _ a -> pretty a) pretty 0
-
-instance (Formula (Sentence v p f) (Sentence v p f), Predicate p, Function f v, Variable v) => HasFixity (Sentence v p f) where
-    fixity = fixityFirstOrder
-
-instance (Formula (Sentence v p f) (Sentence v p f),
-          Variable v, Predicate p, Function f v) =>
-          FirstOrderFormula (Sentence v p f) (Sentence v p f) v where
-    for_all v x = Quantifier ForAll [v] x
-    exists v x = Quantifier ExistsCh [v] x
-    foldFirstOrder qu co tf at f =
-        case f of
-          Not x -> co ((:~:) x)
-          Quantifier op (v:vs) f' ->
-              let op' = case op of
-                          ForAll -> Forall
-                          ExistsCh -> Exists in
-              -- Use Logic.quant' here instead of the constructor
-              -- Quantifier so as not to create quantifications with
-              -- empty variable lists.
-              qu op' v (quant' op' vs f')
-          Quantifier _ [] f' -> foldFirstOrder qu co tf at f'
-          Connective f1 Imply f2 -> co (BinOp f1 (:=>:) f2)
-          Connective f1 Equiv f2 -> co (BinOp f1 (:<=>:) f2)
-          Connective f1 And f2 -> co (BinOp f1 (:&:) f2)
-          Connective f1 Or f2 -> co (BinOp f1 (:|:) f2)
-          Predicate _ _ -> at f
-          Equal _ _ -> at f
-{-
-    zipFirstOrder qu co tf at f1 f2 =
-        case (f1, f2) of
-          (Not f1', Not f2') -> co ((:~:) f1') ((:~:) f2')
-          (Quantifier op1 (v1:vs1) f1', Quantifier op2 (v2:vs2) f2') ->
-              if op1 == op2
-              then let op' = case op1 of
-                               ForAll -> Forall
-                               ExistsCh -> Exists in
-                   qu op' v1 (Quantifier op1 vs1 f1') Forall v2 (Quantifier op2 vs2 f2')
-              else Nothing
-          (Quantifier q1 [] f1', Quantifier q2 [] f2') ->
-              if q1 == q2 then zipFirstOrder qu co tf at f1' f2' else Nothing
-          (Connective l1 op1 r1, Connective l2 op2 r2) ->
-              case (op1, op2) of
-                (And, And) -> co (BinOp l1 (:&:) r1) (BinOp l2 (:&:) r2)
-                (Or, Or) -> co (BinOp l1 (:|:) r1) (BinOp l2 (:|:) r2)
-                (Imply, Imply) -> co (BinOp l1 (:=>:) r1) (BinOp l2 (:=>:) r2)
-                (Equiv, Equiv) -> co (BinOp l1 (:<=>:) r1) (BinOp l2 (:<=>:) r2)
-                _ -> Nothing
-          (Equal _ _, Equal _ _) -> at f1 f2
-          (Predicate _ _, Predicate _ _) -> at f1 f2
-          _ -> Nothing
--}
-
-instance (Variable v, Function f v) => Term (CTerm v f) v f where
-    foldTerm v fn t =
-        case t of
-          Variable x -> v x
-          Function f ts -> fn f ts
-    zipTerms  v f t1 t2 =
-        case (t1, t2) of
-          (Variable v1, Variable v2) -> v v1 v2
-          (Function f1 ts1, Function f2 ts2) -> f f1 ts1 f2 ts2
-          _ -> Nothing
-    vt = Variable
-    fApp f ts = Function f ts
-
-data ConjunctiveNormalForm v p f =
-    CNF [Sentence v p f]
-    deriving (Eq)
-
-data NormalSentence v p f
-    = NFNot (NormalSentence v p f)
-    | NFPredicate p [NormalTerm v f]
-    | NFEqual (NormalTerm v f) (NormalTerm v f)
-    deriving (Eq, Ord, Data, Typeable)
-
--- We need a distinct type here because of the functional dependencies
--- in class FirstOrderFormula.
-data NormalTerm v f
-    = NormalFunction f [NormalTerm v f]
-    | NormalVariable v
-    deriving (Eq, Ord, Data, Typeable)
-
-instance (Constants p, Eq (NormalSentence v p f)) => Constants (NormalSentence v p f) where
-    fromBool x = NFPredicate (fromBool x) []
-    asBool x
-        | fromBool True == x = Just True
-        | fromBool False == x = Just False
-        | True = Nothing
-
-instance Negatable (NormalSentence v p f) where
-    negatePrivate = NFNot
-    foldNegation normal inverted (NFNot x) = foldNegation inverted normal x
-    foldNegation normal _ x = normal x
-
-{-
-instance (Arity p, Constants p, Combinable (NormalSentence v p f)) => Pred p (NormalTerm v f) (NormalSentence v p f) where
-    pApp0 x = NFPredicate x []
-    pApp1 x a = NFPredicate x [a]
-    pApp2 x a b = NFPredicate x [a,b]
-    pApp3 x a b c = NFPredicate x [a,b,c]
-    pApp4 x a b c d = NFPredicate x [a,b,c,d]
-    pApp5 x a b c d e = NFPredicate x [a,b,c,d,e]
-    pApp6 x a b c d e f = NFPredicate x [a,b,c,d,e,f]
-    pApp7 x a b c d e f g = NFPredicate x [a,b,c,d,e,f,g]
-    x .=. y = NFEqual x y
-    x .!=. y = NFNot (NFEqual x y)
--}
-
-instance (Formula (NormalSentence v p f) (NormalSentence v p f),
-          Variable v, Predicate p, Function f v, Combinable (NormalSentence v p f)) => Pretty (NormalSentence v p f) where
-    pretty = prettyFirstOrder (\ _ a -> pretty a) pretty 0
-
-instance (Predicate p, Function f v, Combinable (NormalSentence v p f)) => Formula (NormalSentence v p f) (NormalSentence v p f) where
-    atomic x@(NFPredicate _ _) = x
-    atomic x@(NFEqual _ _) = x
-    atomic _ = error "Chiou: atomic"
-    foldAtoms = foldAtomsFirstOrder
-    mapAtoms = mapAtomsFirstOrder
-
-instance (Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Term (NormalTerm v f) v f,
-          Variable v, Predicate p, Function f v) => FirstOrderFormula (NormalSentence v p f) (NormalSentence v p f) v where
-    for_all _ _ = error "FirstOrderFormula NormalSentence"
-    exists _ _ = error "FirstOrderFormula NormalSentence"
-    foldFirstOrder _ co tf at f =
-        case f of
-          NFNot x -> co ((:~:) x)
-          NFEqual _ _ -> at f
-          NFPredicate p _ -> maybe (at f) tf (asBool p)
-{-
-    zipFirstOrder _ co tf at f1 f2 =
-        case (f1, f2) of
-          (NFNot f1', NFNot f2') -> co ((:~:) f1') ((:~:) f2')
-          (NFEqual _ _, NFEqual _ _) -> at f1 f2
-          (NFPredicate _ _, NFPredicate _ _) -> at f1 f2
-          _ -> Nothing
--}
-
-instance (Formula (NormalSentence v p f) (NormalSentence v p f),
-          Combinable (NormalSentence v p f), Predicate p, Function f v, Variable v) => HasFixity (NormalSentence v p f) where
-    fixity = fixityFirstOrder
-
-instance (Variable v, Function f v) => Term (NormalTerm v f) v f where
-    vt = NormalVariable
-    fApp = NormalFunction
-    foldTerm v f t =
-            case t of
-              NormalVariable x -> v x
-              NormalFunction x ts -> f x ts
-    zipTerms v fn t1 t2 =
-        case (t1, t2) of
-          (NormalVariable x1, NormalVariable x2) -> v x1 x2
-          (NormalFunction f1 ts1, NormalFunction f2 ts2) -> fn f1 ts1 f2 ts2
-          _ -> Nothing
-
-toSentence :: (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Atom (Sentence v p f) (CTerm v f) v, Function f v, Variable v, Predicate p) =>
-              NormalSentence v p f -> Sentence v p f
-toSentence (NFNot s) = (.~.) (toSentence s)
-toSentence (NFEqual t1 t2) = toTerm t1 .=. toTerm t2
-toSentence (NFPredicate p ts) = pApp p (map toTerm ts)
-
-toTerm :: (Variable v, Function f v) => NormalTerm v f -> CTerm v f
-toTerm (NormalFunction f ts) = fApp f (map toTerm ts)
-toTerm (NormalVariable v) = vt v
-
-fromSentence :: forall v p f. (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Predicate p) =>
-                Sentence v p f -> NormalSentence v p f
-fromSentence = foldFirstOrder 
-                 (\ _ _ _ -> error "fromSentence 1")
-                 (\ cm ->
-                      case cm of
-                        ((:~:) f) -> NFNot (fromSentence f)
-                        _ -> error "fromSentence 2")
-                 (\ x -> NFPredicate (fromBool x) [])
-                 (foldAtomEq (\ p ts -> NFPredicate p (map fromTerm ts))
-                             (\ x -> NFPredicate (fromBool x) [])
-                             (\ t1 t2 -> NFEqual (fromTerm t1) (fromTerm t2)))
-
-fromTerm :: CTerm v f -> NormalTerm v f
-fromTerm (Function f ts) = NormalFunction f (map fromTerm ts)
-fromTerm (Variable v) = NormalVariable v
diff --git a/Data/Logic/Tests/Data.hs b/Data/Logic/Tests/Data.hs
--- a/Data/Logic/Tests/Data.hs
+++ b/Data/Logic/Tests/Data.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE DeriveDataTypeable, FlexibleContexts, MonoLocalBinds, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies  #-}
-{-# OPTIONS -fno-warn-name-shadowing -fno-warn-missing-signatures #-}
+{-# OPTIONS -fno-warn-name-shadowing #-}
 module Data.Logic.Tests.Data
     ( tests
     , allFormulas
@@ -920,9 +920,7 @@
                (String, [TestFormula formula atom v]) -> (String, [formula])
 kbKnowledge kb = (fst (kb :: (String, [TestFormula formula atom v])), map formula (snd kb))
 
-proofs :: forall formula atom term v p f. (formula ~ TFormula, atom ~ TAtom, v ~ V,
-                                           FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f, Ord formula, IsString v, IsString p, IsString f) =>
-          [TestProof formula term v]
+proofs :: forall term v f. (Term term v f, IsString v, Ord v) => [TestProof TFormula term v]
 proofs =
     let -- dog = pApp "Dog" :: [term] -> formula
         -- cat = pApp "Cat" :: [term] -> formula
diff --git a/Data/Logic/Tests/Harrison/FOL.hs b/Data/Logic/Tests/Harrison/FOL.hs
--- a/Data/Logic/Tests/Harrison/FOL.hs
+++ b/Data/Logic/Tests/Harrison/FOL.hs
@@ -13,6 +13,7 @@
 import Control.Applicative ((<$>), (<*>))
 import Control.Applicative.Error (Failing(..))
 import Control.Monad (filterM)
+import Data.Logic.Classes.Apply (pApp)
 import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..))
 import Data.Logic.Classes.Constants (false)
 import Data.Logic.Classes.Equals (AtomEq(..), (.=.))
@@ -90,7 +91,7 @@
 -- ------------------------------------------------------------------------- 
 
 example2 :: Formula FOL
-example2 = C.pApp "<" [fApp "+" [vt "x", vt "y"], vt "z"]
+example2 = pApp "<" [fApp "+" [vt "x", vt "y"], vt "z"]
 -- example2 = Atom (R "<" [Fn "+" [Var "x", Var "y"], Var "z"])
 
 -- ------------------------------------------------------------------------- 
@@ -98,8 +99,8 @@
 -- ------------------------------------------------------------------------- 
 
 example3 :: Formula FOL
-example3 = (for_all "x" (C.pApp "<" [vt "x", fApp "2" []] .=>.
-                         C.pApp "<=" [fApp "*" [fApp "2" [], vt "x"], fApp "3" []])) .|. false
+example3 = (for_all "x" (pApp "<" [vt "x", fApp "2" []] .=>.
+                         pApp "<=" [fApp "*" [fApp "2" [], vt "x"], fApp "3" []])) .|. false
 example4 :: TermType
 example4 = fApp "*" [fApp "2" [], vt "x"]
 
diff --git a/Data/Logic/Tests/Harrison/Prop.hs b/Data/Logic/Tests/Harrison/Prop.hs
--- a/Data/Logic/Tests/Harrison/Prop.hs
+++ b/Data/Logic/Tests/Harrison/Prop.hs
@@ -8,7 +8,6 @@
 import Data.Logic.Classes.Constants (true, false)
 import Data.Logic.Classes.Formula (atomic)
 import Data.Logic.Classes.Negate ((.~.), (¬))
-import Data.Logic.Classes.Propositional
 import Data.Logic.Harrison.Lib ((|=>))
 import Data.Logic.Harrison.Prop (eval, atoms, truthTable, tautology, pSubst, psimplify,
                                  nnf, dnf', rawdnf, dual, purednf, trivial, cnf')
diff --git a/changelog b/changelog
--- a/changelog
+++ b/changelog
@@ -1,3 +1,11 @@
+haskell-logic-classes (1.5) unstable; urgency=low
+
+  * Move the pApp* functions from Data.Logic.Classes.FirstOrder to
+    Data.Logic.Classes.Apply, and let them work with any formula,
+    not just first order.
+
+ -- David Fox <dsf@seereason.com>  Sat, 29 Mar 2014 07:57:37 -0700
+
 haskell-logic-classes (1.4.8) unstable; urgency=low
 
   * Make changelog visible in hackage.
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.8
+Version:          1.5
 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
@@ -53,7 +53,7 @@
                    Data.Logic.Harrison.Skolem
                    Data.Logic.Harrison.Tableaux
                    Data.Logic.Harrison.Unif
-                   Data.Logic.Instances.Chiou
+                   -- Data.Logic.Instances.Chiou
                    Data.Logic.Instances.PropLogic
                    Data.Logic.Instances.SatSolver
                    -- Data.Logic.Instances.TPTP