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
@@ -18,6 +18,7 @@
 import Data.Logic.Classes.Pretty (HasFixity(..), Fixity(..), FixityDirection(..))
 import qualified Data.Logic.Classes.Propositional as P
 import Data.Logic.Classes.Negate
+import Data.Logic.Harrison.Lib ({- instance Monad 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/Lib.hs b/Data/Logic/Harrison/Lib.hs
--- a/Data/Logic/Harrison/Lib.hs
+++ b/Data/Logic/Harrison/Lib.hs
@@ -1,7 +1,8 @@
-{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeriveDataTypeable, RankNTypes, StandaloneDeriving #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-binds #-}
 module Data.Logic.Harrison.Lib
-    ( tests
+    ( failing
+    , tests
     , setAny
     , setAll
     -- , itlist2
@@ -34,11 +35,34 @@
     , (∅)
     ) where
 
-import Control.Applicative.Error (Failing(..), failing)
+import Control.Applicative.Error (Failing(..), ErrorMsg)
+import Data.Generics
 import qualified Data.Map as Map
 import Data.Maybe
 import qualified Data.Set as Set
 import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)
+
+-- | Case analysis for the 'Failing' type, from unpublished changes to 
+-- the applicative-extras packages.  If the value is @'Failure'@, apply 
+-- the first function to @[ErrorMsg]@; if it is @'Success' a@, apply 
+-- the second function to @a@.
+failing :: ([ErrorMsg] -> b) -> (a -> b) -> Failing a -> b
+failing f _ (Failure errs) = f errs
+failing _ f (Success a)    = f a
+ 
+instance Monad Failing where
+  return = Success
+  m >>= f =
+      case m of
+        (Failure errs) -> (Failure errs)
+        (Success a) -> f a
+  fail errMsg = Failure [errMsg]
+  
+deriving instance Typeable1 Failing
+deriving instance Data a => Data (Failing a)
+deriving instance Read a => Read (Failing a)
+deriving instance Eq a => Eq (Failing a)
+deriving instance Ord a => Ord (Failing a)
 
 (∅) :: Set.Set a
 (∅) = Set.empty
diff --git a/Data/Logic/Harrison/Normal.hs b/Data/Logic/Harrison/Normal.hs
--- a/Data/Logic/Harrison/Normal.hs
+++ b/Data/Logic/Harrison/Normal.hs
@@ -9,14 +9,13 @@
     , simpcnf'
     ) where
 
-import Control.Applicative.Error (failing)
 import Data.Logic.Classes.Combine (Combination(..), BinOp(..))
 import Data.Logic.Classes.Constants (Constants(..))
 import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))
 import Data.Logic.Classes.Formula (Formula(atomic))
 import Data.Logic.Classes.Literal (Literal, fromFirstOrder)
 import Data.Logic.Classes.Negate (Negatable, negated, (.~.))
-import Data.Logic.Harrison.Lib (setAny, allpairs)
+import Data.Logic.Harrison.Lib (setAny, allpairs, failing)
 import Data.Logic.Harrison.Skolem (nnf)
 import qualified Data.Set.Extra as Set
 import Prelude hiding (negate)
diff --git a/Data/Logic/Harrison/Resolution.hs b/Data/Logic/Harrison/Resolution.hs
--- a/Data/Logic/Harrison/Resolution.hs
+++ b/Data/Logic/Harrison/Resolution.hs
@@ -8,7 +8,7 @@
     , matchAtomsEq
     ) where
 
-import Control.Applicative.Error (Failing(..), failing)
+import Control.Applicative.Error (Failing(..))
 import Data.Logic.Classes.Atom (Atom(match))
 import Data.Logic.Classes.Combine (Combination(..))
 import Data.Logic.Classes.Equals (AtomEq, zipAtomsEq)
@@ -20,7 +20,7 @@
 import Data.Logic.Classes.Variable (Variable(prefix))
 import Data.Logic.Harrison.FOL (subst, fv, generalize, list_disj, list_conj)
 import Data.Logic.Harrison.Lib (settryfind, allpairs, allsubsets, setAny, setAll,
-                                allnonemptysubsets, (|->), apply, defined)
+                                allnonemptysubsets, (|->), apply, defined, failing)
 import Data.Logic.Harrison.Normal (simpdnf, simpcnf, trivial)
 import Data.Logic.Harrison.Skolem (pnf, SkolemT, askolemize, specialize)
 import Data.Logic.Harrison.Tableaux (unify_literals)
diff --git a/Data/Logic/Harrison/Unif.hs b/Data/Logic/Harrison/Unif.hs
--- a/Data/Logic/Harrison/Unif.hs
+++ b/Data/Logic/Harrison/Unif.hs
@@ -6,8 +6,9 @@
     , unifyAndApply
     ) where
 
-import Control.Applicative.Error (Failing(..), failing)
+import Control.Applicative.Error (Failing(..))
 import Data.Logic.Classes.Term (Term(..), tsubst)
+import Data.Logic.Harrison.Lib (failing)
 import qualified Data.Map as Map
 {-
 (* ========================================================================= *)
diff --git a/Data/Logic/Tests/Harrison/Unif.hs b/Data/Logic/Tests/Harrison/Unif.hs
--- a/Data/Logic/Tests/Harrison/Unif.hs
+++ b/Data/Logic/Tests/Harrison/Unif.hs
@@ -4,8 +4,9 @@
     ( tests
     ) where
 
-import Control.Applicative.Error (Failing(..), failing)
+import Control.Applicative.Error (Failing(..))
 import Data.Logic.Classes.Term (Term(fApp, vt), tsubst)
+import Data.Logic.Harrison.Lib (failing)
 import Data.Logic.Harrison.Unif (fullUnify)
 import Data.Logic.Tests.HUnit ()
 import Data.Logic.Types.Harrison.FOL (TermType)
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.4
+Version:          1.4.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