diff --git a/Main.hs b/Main.hs
index abb53f8..05f0a60 100644
--- a/Main.hs
+++ b/Main.hs
@@ -257,10 +257,10 @@ compileFull inputFile moutputFile
           let cFile = outputFile ++ extension
               hFile = outputFile ++ ".h"
               iFile = outputFile ++ ".inc"
+          lift $ modify $ \cs -> cs { csOutputIncFile = Just iFile }
           lift $ withOutputFile cFile $ \hb ->
             withOutputFile hFile $ \hh ->
-              withOutputFile iFile $ \hi ->
-                compile ModeCompile inputFile ((hb, hh, hi), hFile)
+                compile ModeCompile inputFile ((hb, hh), hFile)
           noteFile cFile
           when (csRunIndent optsPS) $
             exec $ "indent " ++ cFile
@@ -282,7 +282,7 @@ compileFull inputFile moutputFile
                  exec $ cCommand sFile oFile (csCompilerFlags optsPS)
                  -- Analyse the assembly for stack sizes, and output a
                  -- "post" C file
-                 lift $ withOutputFile postCFile $ \h -> postCAnalyse sFile ((h,intErr,intErr),intErr)
+                 lift $ withOutputFile postCFile $ \h -> postCAnalyse sFile ((h,intErr),intErr)
                  -- Compile this new "post" C file into an object file
                  exec $ cCommand postCFile postOFile (csCompilerFlags optsPS)
                  -- Link the object files into a binary
@@ -325,13 +325,12 @@ compileFull inputFile moutputFile
                     ExitFailure n -> dieReport (Nothing, "Command \"" ++ cmd ++ "\" failed: exited with code: " ++ show n)
 
 -- | Picks out the handle from the options and passes it to the function:
-useOutputOptions :: (((Handle, Handle, Handle), String) -> PassM ()) -> PassM ()
+useOutputOptions :: (((Handle, Handle), String) -> PassM ()) -> PassM ()
 useOutputOptions func
   =  do optsPS <- get
         withHandleFor (csOutputFile optsPS) $ \hb ->
           withHandleFor (csOutputHeaderFile optsPS) $ \hh ->
-            withHandleFor (csOutputIncFile optsPS) $ \hi ->
-              func ((hb, hh, hi), csOutputHeaderFile optsPS)
+              func ((hb, hh), csOutputHeaderFile optsPS)
   where
     withHandleFor "-" func = func stdout
     withHandleFor file func =
@@ -376,11 +375,12 @@ showTokens html ts = evalState (mapM showToken ts >>* spaceOut) 0
                             then ("&nbsp;", "<br/>\n", \s -> "<b>" ++ s ++ "</b>")
                             else (" ", "\n", id)
 
+
 -- | Compile a file.
 -- This is written in the PassM monad -- as are most of the things it calls --
 -- because then it's very easy to pass the state around.
-compile :: CompMode -> String -> ((Handle, Handle, Handle), String) -> PassM ()
-compile mode fn (outHandles@(outHandle, _, _), headerName)
+compile :: CompMode -> String -> ((Handle, Handle), String) -> PassM ()
+compile mode fn (outHandles@(outHandle, _), headerName)
   =  do optsPS <- get
 
         debug "{{{ Parse"
@@ -441,8 +441,8 @@ compile mode fn (outHandles@(outHandle, _, _), headerName)
         progress "Done"
 
 -- | Analyse an assembly file.
-postCAnalyse :: String -> ((Handle, Handle, Handle), String) -> PassM ()
-postCAnalyse fn ((outHandle, _, _), _)
+postCAnalyse :: String -> ((Handle, Handle), String) -> PassM ()
+postCAnalyse fn ((outHandle, _), _)
     =  do asm <- liftIO $ readFile fn
 
           progress "Analysing assembly"
diff --git a/backends/GenerateC.hs b/backends/GenerateC.hs
index 9ed76d2..acdfa3c 100644
--- a/backends/GenerateC.hs
+++ b/backends/GenerateC.hs
@@ -155,7 +155,7 @@ cgenOps = GenOps {
 --}}}
 
 --{{{  top-level
-generateC :: (Handle, Handle, Handle) -> String -> A.AST -> PassM ()
+generateC :: (Handle, Handle) -> String -> A.AST -> PassM ()
 generateC = generate cgenOps
 
 cgenTopLevel :: String -> A.AST -> CGen ()
diff --git a/backends/GenerateCBased.hs b/backends/GenerateCBased.hs
index 040e174..2d46fa8 100644
--- a/backends/GenerateCBased.hs
+++ b/backends/GenerateCBased.hs
@@ -58,7 +58,6 @@ type CGenOutput = Either [String] Handle
 data CGenOutputs = CGenOutputs
   { cgenBody :: CGenOutput
   , cgenHeader :: CGenOutput
-  , cgenOccamInc :: CGenOutput
   }
 
 --{{{  monad definition
@@ -246,10 +245,10 @@ fget :: (GenOps -> a) -> CGen a
 fget = asks
 
 -- Handles are body, header, occam-inc
-generate :: GenOps -> (Handle, Handle, Handle) -> String -> A.AST -> PassM ()
-generate ops (hb, hh, hi) hname ast
+generate :: GenOps -> (Handle, Handle) -> String -> A.AST -> PassM ()
+generate ops (hb, hh) hname ast
   = evalStateT (runReaderT (call genTopLevel hname ast) ops)
-      (CGenOutputs (Right hb) (Right hh) (Right hi))
+      (CGenOutputs (Right hb) (Right hh))
 
 genComma :: CGen ()
 genComma = tell [","]
diff --git a/backends/GenerateCPPCSP.hs b/backends/GenerateCPPCSP.hs
index 2089465..df08ab8 100644
--- a/backends/GenerateCPPCSP.hs
+++ b/backends/GenerateCPPCSP.hs
@@ -122,7 +122,7 @@ chansToAny = cppOnlyPass "Transform channels to ANY"
 
 --{{{  top-level
 -- | Transforms the given AST into a pass that generates C++ code.
-generateCPPCSP :: (Handle, Handle, Handle) -> String -> A.AST -> PassM ()
+generateCPPCSP :: (Handle, Handle) -> String -> A.AST -> PassM ()
 generateCPPCSP = generate cppgenOps
 
 cppcspPrereq :: [Property]
diff --git a/data/CompState.hs b/data/CompState.hs
index 329ef1d..2696b40 100644
--- a/data/CompState.hs
+++ b/data/CompState.hs
@@ -106,7 +106,7 @@ data CompState = CompState {
     csVerboseLevel :: Int,
     csOutputFile :: String,
     csOutputHeaderFile :: String,
-    csOutputIncFile :: String,
+    csOutputIncFile :: Maybe String,
     csKeepTemporaries :: Bool,
     csEnabledWarnings :: Set WarningType,
     csRunIndent :: Bool,
@@ -156,7 +156,7 @@ emptyState = CompState {
     csVerboseLevel = 0,
     csOutputFile = "-",
     csOutputHeaderFile = "-",
-    csOutputIncFile = "-",
+    csOutputIncFile = Nothing,
     csKeepTemporaries = False,
     csEnabledWarnings = Set.fromList
       [ WarnInternal
diff --git a/frontends/OccamPasses.hs b/frontends/OccamPasses.hs
index feb26dd..fa173b0 100644
--- a/frontends/OccamPasses.hs
+++ b/frontends/OccamPasses.hs
@@ -21,6 +21,10 @@ module OccamPasses (occamPasses, foldConstants, checkConstants) where
 
 import Control.Monad.State
 import Data.Generics
+import Data.List
+import qualified Data.Sequence as Seq
+import qualified Data.Foldable as F
+import System.IO
 
 import qualified AST as A
 import CompState
@@ -46,9 +50,40 @@ occamPasses =
     , checkConstants
     , resolveAmbiguities
     , checkTypes
+    , writeIncFile
     , pushUpDirections
     ]
 
+writeIncFile :: Pass
+writeIncFile = occamOnlyPass "Write .inc file" [] []
+  (passOnlyOnAST "writeIncFile" (\t ->
+    do out <- getCompState >>* csOutputIncFile
+       case out of
+         Just fn -> do f <- liftIO $ openFile fn WriteMode
+                       contents <- emitProcsAsExternal t >>* (unlines . F.toList)
+                       liftIO $ hPutStr f contents
+                       liftIO $ hClose f
+         Nothing -> return ()
+       return t
+  ))
+  where
+    emitProcsAsExternal :: A.AST -> PassM (Seq.Seq String)
+    emitProcsAsExternal (A.Spec _ (A.Specification _ n (A.Proc _ _ fs _)) scope)
+      = do thisProc <- sequence (
+             [return "#PRAGMA EXTERNAL \"PROC "
+             ,showCode n
+             ,return "("
+             ] ++ intersperse (return ",") (map showCode fs) ++
+             [return ") = 42\""
+             ]) >>* concat
+           emitProcsAsExternal scope >>* (thisProc Seq.<|)
+    emitProcsAsExternal (A.Spec _ _ scope) = emitProcsAsExternal scope
+    emitProcsAsExternal (A.ProcThen _ _ scope) = emitProcsAsExternal scope
+    emitProcsAsExternal (A.Only {}) = return Seq.empty
+    emitProcsAsExternal (A.Several _ ss)
+      = foldl (liftM2 (Seq.><)) (return Seq.empty) (map emitProcsAsExternal ss)
+
+
 -- | Fixed the types of array constructors according to the replicator count
 fixConstructorTypes :: Pass
 fixConstructorTypes = occamOnlyPass "Fix the types of array constructors"