diff --git a/haskell/README.md b/haskell/README.md
index d608bdbe9..2c1e41df2 100644
--- a/haskell/README.md
+++ b/haskell/README.md
@@ -21,23 +21,23 @@ To build it:
   - install `Cabal 1.18` or later. This is included with GHC 7.8. 
   - configure the sources:
   
-        runhaskell Setup.hs configure --with-target=<arch>-<platform>
-        
-    Valid target options are: `arm-qemu`, `arm-lyrebird`
-    
+        runhaskell Setup.hs configure --with-target=arm-qemu
+
+Further target options may be supported again in the future.
+
   - build the library:
   
         runhaskell Setup.hs build
-        
+
   - install:
   
         runhaskell Setup.hs install --user
 
 
 After that, you can compile Haskell programs using the simulator by adding
-`-package SEL4` to the `ghc` command line. Note that the qemu and lyrebird
-targets require some callback functions to be accessible via the FFI, so
-it is not possible to load a model compiled for those targets in GHCi.
+`-package SEL4` to the `ghc` command line. Note that the qemu target requires
+some callback functions to be accessible via the FFI, so it is not possible to
+load a model compiled for those targets in GHCi.
 
 Currently, the simulator interface is out of date, so this model is currently
 only useful as documentation and as intermediate artefact in the seL4
diff --git a/haskell/SEL4.cabal b/haskell/SEL4.cabal
index cf08c0c6a..4befa0fbb 100644
--- a/haskell/SEL4.cabal
+++ b/haskell/SEL4.cabal
@@ -13,7 +13,7 @@ version:                1.4-pre
 cabal-version:          >= 1.8
 build-type:             Simple
 license:                AllRightsReserved
-author:                 Philip Derrin et. al.
+author:                 Philip Derrin et. al., NICTA
 synopsis:               Executable specification for the seL4 Kernel
 tested-with:            GHC == 7.8.3
 
diff --git a/haskell/Setup.hs b/haskell/Setup.hs
index 5cbbe999c..9ebfeba68 100644
--- a/haskell/Setup.hs
+++ b/haskell/Setup.hs
@@ -10,8 +10,6 @@
 -- @TAG(GD_GPL)
 --
 
--- This is to shut GHC up about defaultUserHooks.
-
 module Main where
 import Control.Applicative((<$>))
 import Distribution.Simple
@@ -28,8 +26,7 @@ import Data.List(isPrefixOf, find)
 import Control.Monad(unless, liftM)
 
 targets =
-    [ ("arm-qemu",     ("ARM", "QEmu"))
-    , ("arm-lyrebird", ("ARM", "Lyrebird"))]
+    [ ("arm-qemu",     ("ARM", "QEmu")) ]
 
 bootModules =
     [ "Kernel/CSpace"
@@ -86,10 +83,6 @@ main = do
     let targetArg = find (targetPrefix `isPrefixOf`) args
     let targetName = liftM (drop (length targetPrefix)) targetArg
     let args' = filter (not . isPrefixOf targetPrefix) args
-              -- n.b.  GHC 7.0.3 whinges about defaultUserHooks being
-              -- deprecated, and demands simpleUserHooks or autoconfUserHooks
-              -- instead.  Neither of those actually works here, so I'm stuck
-              -- with defaultUserHooks.
     let hooks = simpleUserHooks {
                     preBuild = \args flags -> do
                         generateHSBoot
diff --git a/haskell/src/SEL4/Machine/Hardware/ARM/Lyrebird.hs b/haskell/src/SEL4/Machine/Hardware/ARM/Lyrebird.hs
deleted file mode 100644
index f85637a9e..000000000
--- a/haskell/src/SEL4/Machine/Hardware/ARM/Lyrebird.hs
+++ /dev/null
@@ -1,119 +0,0 @@
---
--- Copyright 2014, General Dynamics C4 Systems
---
--- This software may be distributed and modified according to the terms of
--- the GNU General Public License version 2. Note that NO WARRANTY is provided.
--- See "LICENSE_GPLv2.txt" for details.
---
--- @TAG(GD_GPL)
---
-
-{-# LANGUAGE EmptyDataDecls, ForeignFunctionInterface,
-             GeneralizedNewtypeDeriving #-}
-
-module SEL4.Machine.Hardware.ARM.Lyrebird where
-
-import SEL4.Machine.RegisterSet
-import Foreign.Ptr
-import Data.Ix
-import Data.Word(Word8)
-import Data.Bits
-
-data CallbackData
-
-data IRQ = TimerInterrupt
-    deriving (Enum, Bounded, Ord, Ix, Eq, Show)
-
-newtype PAddr = PAddr { fromPAddr :: Word }
-    deriving (Show, Eq, Ord, Bounded, Real, Enum, Integral, Num, Bits, FiniteBits)
-
-ptrFromPAddr :: PAddr -> PPtr a
-ptrFromPAddr (PAddr addr) = PPtr addr
-
-addrFromPPtr :: PPtr a -> PAddr
-addrFromPPtr (PPtr ptr) = PAddr ptr
-
-pageColourBits :: Int
-pageColourBits = 0
-
-foreign import ccall "arm_get_mem_top"
-    getMemorySize :: Ptr CallbackData -> IO Int
-
-getMemoryRegions :: Ptr CallbackData -> IO [(PAddr, PAddr)]
-getMemoryRegions env = do
-        size <- getMemorySize env
-        return [(PAddr 0, PAddr (bit size))]
-
-getDeviceRegions :: Ptr CallbackData -> IO [(PAddr, PAddr)]
-getDeviceRegions _ = return []
-
-getKernelDevices :: Ptr CallbackData -> IO [(PAddr, PPtr Word)]
-getKernelDevices _ = return []
-
-maskInterrupt :: Ptr CallbackData -> Bool -> IRQ -> IO ()
-maskInterrupt env bool _ = maskIRQCallback env bool
-
-ackInterrupt :: Ptr CallbackData -> IRQ -> IO ()
-ackInterrupt env _ = ackIRQCallback env
-
-foreign import ccall "arm_check_interrupt"
-    getInterruptState :: Ptr CallbackData -> IO Bool
-
-foreign import ccall "arm_mask_interrupt"
-    maskIRQCallback :: Ptr CallbackData -> Bool -> IO ()
-
-foreign import ccall "arm_ack_interrupt"
-    ackIRQCallback :: Ptr CallbackData -> IO ()
-
-getActiveIRQ :: Ptr CallbackData -> IO (Maybe IRQ)
-getActiveIRQ env = do
-    timer_irq <- getInterruptState env
-    return $ if timer_irq then Just TimerInterrupt else Nothing
-
-configureTimer :: Ptr CallbackData -> IO IRQ
-configureTimer _ = return TimerInterrupt
-
-resetTimer :: Ptr CallbackData -> IO ()
-resetTimer _ = return ()
-
-foreign import ccall unsafe "arm_load_word"
-    loadWordCallback :: Ptr CallbackData -> PAddr -> IO Word
-
-foreign import ccall unsafe "arm_store_word"
-    storeWordCallback :: Ptr CallbackData -> PAddr -> Word -> IO ()
-
-foreign import ccall unsafe "arm_tlb_flush"
-    invalidateTLBCallback :: Ptr CallbackData -> IO ()
-
-foreign import ccall unsafe "arm_tlb_flush_asid"
-    invalidateHWASIDCallback :: Ptr CallbackData -> Word8 -> IO ()
-
-foreign import ccall unsafe "arm_tlb_flush_vptr"
-    invalidateMVACallback :: Ptr CallbackData -> Word -> IO ()
-
-cacheCleanMVACallback :: Ptr CallbackData -> PPtr a -> IO ()
-cacheCleanMVACallback _cptr _mva = return ()
-
-cacheCleanRangeCallback :: Ptr CallbackData -> PPtr a -> PPtr a -> IO ()
-cacheCleanRangeCallback _cptr _vbase _vtop = return ()
-
-cacheCleanCallback :: Ptr CallbackData -> IO ()
-cacheCleanCallback _cptr = return ()
-
-cacheInvalidateRangeCallback :: Ptr CallbackData -> PPtr a -> PPtr a -> IO ()
-cacheInvalidateRangeCallback _cptr _vbase _vtop = return ()
-
-foreign import ccall unsafe "arm_set_asid"
-    setHardwareASID :: Ptr CallbackData -> Word8 -> IO ()
-
-foreign import ccall unsafe "arm_set_table_root"
-    setCurrentPD :: Ptr CallbackData -> PAddr -> IO ()
-
-foreign import ccall unsafe "arm_get_ifsr"
-    getIFSR :: Ptr CallbackData -> IO Word
-
-foreign import ccall unsafe "arm_get_dfsr"
-    getDFSR :: Ptr CallbackData -> IO Word
-
-foreign import ccall unsafe "arm_get_far"
-    getFAR :: Ptr CallbackData -> IO VPtr