diff --git a/src/Theory/Constraint/System.hs b/src/Theory/Constraint/System.hs
--- a/src/Theory/Constraint/System.hs
+++ b/src/Theory/Constraint/System.hs
@@ -140,6 +140,18 @@
     show UntypedCaseDist = "untyped"
     show TypedCaseDist   = "typed"
 
+-- Adapted from the output of 'derive'.
+instance Read CaseDistKind where
+        readsPrec p0 r
+          = readParen (p0 > 10)
+              (\ r0 ->
+                 [(UntypedCaseDist, r1) | ("untyped", r1) <- lex r0])
+              r
+              ++
+              readParen (p0 > 10)
+                (\ r0 -> [(TypedCaseDist, r1) | ("typed", r1) <- lex r0])
+                r
+
 instance Ord CaseDistKind where
     compare UntypedCaseDist UntypedCaseDist = EQ
     compare UntypedCaseDist TypedCaseDist   = LT
diff --git a/src/Theory/Text/Parser.hs b/src/Theory/Text/Parser.hs
--- a/src/Theory/Text/Parser.hs
+++ b/src/Theory/Text/Parser.hs
@@ -47,7 +47,8 @@
 
 -- | Parse a security protocol theory file.
 parseOpenTheory :: [String] -- ^ Defined flags
-                -> FilePath -> IO OpenTheory
+                -> FilePath
+                -> IO OpenTheory
 parseOpenTheory flags = parseFile (theory flags)
 
 -- | Parse DH intruder rules.
@@ -57,11 +58,11 @@
 -- | Parse a security protocol theory from a string.
 parseOpenTheoryString :: [String]  -- ^ Defined flags.
                       -> String -> Either ParseError OpenTheory
-parseOpenTheoryString flags = parseFromString (theory flags)
+parseOpenTheoryString flags = parseString "<unknown source>" (theory flags)
 
 -- | Parse a lemma for an open theory from a string.
 parseLemma :: String -> Either ParseError (Lemma ProofSkeleton)
-parseLemma = parseFromString lemma
+parseLemma = parseString "<unknown source>" lemma
 
 ------------------------------------------------------------------------------
 -- Parsing Terms
diff --git a/src/Theory/Text/Parser/Token.hs b/src/Theory/Text/Parser/Token.hs
--- a/src/Theory/Text/Parser/Token.hs
+++ b/src/Theory/Text/Parser/Token.hs
@@ -81,7 +81,7 @@
     -- * Basic Parsing
   , Parser
   , parseFile
-  , parseFromString
+  , parseString
   ) where
 
 import           Prelude             hiding (id, (.))
@@ -99,10 +99,6 @@
 import           Theory
 
 
-
-
-
-
 ------------------------------------------------------------------------------
 -- Parser
 ------------------------------------------------------------------------------
@@ -129,20 +125,22 @@
       , T.caseSensitive  = True
       }
 
--- | Parse a file.
+-- | Run a parser on the contents of a file.
 parseFile :: Parser a -> FilePath -> IO a
-parseFile parser f = do
-  s <- readFile f
-  case runParser (T.whiteSpace spthy *> parser) minimalMaudeSig f s of
-    Right p -> return p
-    Left err -> error $ show err
+parseFile parser inFile = do
+    inp <- readFile inFile
+    case parseString inFile parser inp of
+        Right x  -> return x
+        Left err -> error $ show err
 
 -- | Run a given parser on a given string.
-parseFromString :: Parser a -> String -> Either ParseError a
-parseFromString parser =
-    runParser (T.whiteSpace spthy *> parser) minimalMaudeSig dummySource
-  where
-    dummySource = "<interactive>"
+parseString :: FilePath
+            -- ^ Description of the source file. (For error reporting.)"
+            -> Parser a
+            -> String         -- ^ Input string.
+            -> Either ParseError a
+parseString srcDesc parser =
+    runParser (T.whiteSpace spthy *> parser) minimalMaudeSig srcDesc
 
 
 -- Token parsers
diff --git a/tamarin-prover-theory.cabal b/tamarin-prover-theory.cabal
--- a/tamarin-prover-theory.cabal
+++ b/tamarin-prover-theory.cabal
@@ -2,7 +2,7 @@
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            0.8.4.0
+version:            0.8.5.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -38,30 +38,30 @@
 
     build-depends:
         base              == 4.*
-      , bytestring        == 0.9.*
-      , deepseq           == 1.3.*
-      , array             >= 0.3   && < 0.5
-      , containers        >= 0.4.2 && < 0.5
-      , dlist             == 0.5.*
-      , mtl               == 2.0.*
+      , bytestring        >= 0.9
+      , deepseq           >= 1.3
+      , array             >= 0.3  
+      , containers        >= 0.4.2
+      , dlist             >= 0.5
+      , mtl               >= 2.1
       , cmdargs           == 0.10.*
-      , filepath          >= 1.1   && < 1.4
-      , directory         >= 1.0   && < 1.2
-      , process           == 1.1.*
+      , filepath          >= 1.1
+      , directory         >= 1.0
+      , process           >= 1.1
       , parsec            == 3.1.*
       , safe              >= 0.2  && < 0.4
-      , transformers      == 0.2.*
-      , fclabels          == 1.1.*
+      , transformers      >= 0.3
+      , fclabels          == 1.*
       , uniplate          == 1.6.*
-      , syb               == 0.3.* && >= 0.3.3
+      , syb               >= 0.3.3
       , binary            == 0.5.*
       , derive            == 2.5.*
-      , time              >= 1.2   && < 1.5
-      , parallel          == 3.2.*
-      , HUnit             == 1.2.*
+      , time              >= 1.2 
+      , parallel          >= 3.2
+      , HUnit             >= 1.2
 
-      , tamarin-prover-utils >= 0.8.4  && < 0.9
-      , tamarin-prover-term  >= 0.8.4  && < 0.9
+      , tamarin-prover-utils >= 0.8.5  && < 0.9
+      , tamarin-prover-term  >= 0.8.5  && < 0.9
 
 
     hs-source-dirs: src