diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,32 +1,30 @@
-Copyright (c) 2005 Lennart Augustsson, Thomas Johnsson
-    Chalmers University of Technology
+Copyright (c) 2005-2014, Lennart Augustsson
 All rights reserved.
 
-This code is derived from software written by Lennart Augustsson
-(lennart@augustsson.net).
-
 Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions
-are met:
-1. Redistributions of source code must retain the above copyright
-   notice, this list of conditions and the following disclaimer.
-2. Redistributions in binary form must reproduce the above copyright
-   notice, this list of conditions and the following disclaimer in the
-   documentation and/or other materials provided with the distribution.
-3. None of the names of the copyright holders may be used to endorse
-   or promote products derived from this software without specific
-   prior written permission.
+modification, are permitted provided that the following conditions are
+met:
 
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
-EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
-PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
-LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
-CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
-SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
-BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
-WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
-OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
-IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
 
-*** End of disclaimer. ***
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Lennart Augustsson nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/djinn.cabal b/djinn.cabal
--- a/djinn.cabal
+++ b/djinn.cabal
@@ -1,22 +1,28 @@
-Name:		djinn
-Version:	2011.7.23
-License:	BSD3
-License-file:	LICENSE
-Author:		Lennart Augustsson
-Maintainer:	lennart@augustsson.net
-Description:	Djinn uses an theorem prover for intuitionistic propositional logic
-		to generate a Haskell expression when given a type.
-Category:	source-tools
-Homepage:	http://www.augustsson.net/Darcs/Djinn/
-Synopsis:	Generate Haskell code from a type
-Build-type:	Simple
-Build-Depends:	base >= 4 && < 5, mtl, haskeline -any, pretty, array, containers
+Name:           djinn
+Version:        2014.9.7
+Synopsis:       Generate Haskell code from a type
+Description:    Djinn uses an theorem prover for intuitionistic propositional logic
+                to generate a Haskell expression when given a type.
+Bug-reports:    https://github.com/haskell/augustss/djinn/issues
+License:        BSD3
+License-File:   LICENSE
+Author:         Lennart Augustsson
+Maintainer:     Lennart Augustsson
+Copyright:      2014 Lennart Augustsson
+Category:       source-tools
+Build-type:     Simple
+Cabal-Version:  >= 1.8
+Stability:      experimental
 
-Executable:     djinn
-Main-Is:        Djinn.hs
-Hs-Source-Dirs: src
-Other-modules:  Help, HCheck,  LJT, HTypes, LJTFormula, REPL
+source-repository head
+  type:     git
+  location: https://github.com/augustss/djinn
 
-ghc-options:         -O2 -Wall -optl-Wl
---ghc-options:         -Wall -optl-Wl
-ghc-prof-options:    -prof -auto-all
+executable djinn
+  Main-Is:        Djinn.hs
+
+  Build-Depends:  base >= 4 && < 6, mtl, haskeline -any, pretty, array, containers
+
+  Other-modules:  Help, HCheck,  LJT, HTypes, LJTFormula, REPL
+
+  Hs-Source-Dirs: src
diff --git a/src/LJT.hs b/src/LJT.hs
--- a/src/LJT.hs
+++ b/src/LJT.hs
@@ -20,6 +20,7 @@
 module LJT (module LJTFormula, provable,
             prove, Proof) where
 
+import Control.Applicative(Applicative(..), Alternative(empty, (<|>)))
 import Control.Monad
 import Data.List (partition)
 import Debug.Trace
@@ -138,6 +139,10 @@
 -- results.  But this is much better for backtracking.
 newtype P a = P { unP :: PS -> [(PS, a)] }
 
+instance Applicative P where
+    pure = return
+    (<*>) = ap
+
 instance Monad P where
     return x = P $ \ s -> [(s, x)]
     P m >>= f = P $ \ s ->
@@ -146,6 +151,10 @@
 instance Functor P where
     fmap f (P m) = P $ \ s ->
         [ (s', f x) | (s', x) <- m s ]
+
+instance Alternative P where
+    empty = mzero
+    (<|>) = mplus
 
 instance MonadPlus P where
     mzero = P $ \ _s -> []