diff --git a/backends/BackendPasses.hs b/backends/BackendPasses.hs
index ec55a12..8dce7a9 100644
--- a/backends/BackendPasses.hs
+++ b/backends/BackendPasses.hs
@@ -110,6 +110,7 @@ declareSizesArray = occamOnlyPass "Declare array-size arrays"
                                  , A.ndOrigName = A.nameName n
                                  , A.ndSpecType = spec
                                  , A.ndAbbrevMode = A.ValAbbrev
+                                 , A.ndNameSource = A.NameNonce
                                  , A.ndPlacement = A.Unplaced
                                  }
 
@@ -279,6 +280,7 @@ addSizesFormalParameters = occamOnlyPass "Add array-size arrays to PROC headers"
                         ,A.ndOrigName = A.nameName n
                         ,A.ndSpecType = A.Declaration m t
                         ,A.ndAbbrevMode = A.ValAbbrev
+                        ,A.ndNameSource = A.NameNonce
                         ,A.ndPlacement = A.Unplaced}
     
     transformFormals :: Meta -> [A.Formal] -> PassM ([A.Formal], [A.Formal])
diff --git a/backends/BackendPassesTest.hs b/backends/BackendPassesTest.hs
index 1e56b41..d3a5bc6 100644
--- a/backends/BackendPassesTest.hs
+++ b/backends/BackendPassesTest.hs
@@ -326,6 +326,7 @@ defineTestName n sp am
          ,A.ndOrigName = n
          ,A.ndSpecType = sp
          ,A.ndAbbrevMode = am
+         ,A.ndNameSource = A.NameUser
          ,A.ndPlacement = A.Unplaced
          }
 
diff --git a/backends/GenerateCTest.hs b/backends/GenerateCTest.hs
index 03473d8..74e0ed2 100644
--- a/backends/GenerateCTest.hs
+++ b/backends/GenerateCTest.hs
@@ -756,7 +756,10 @@ testRetypeSizes = TestList
    over = local $ \ops -> ops {genBytesIn = showBytesInParams, genStop = override2 at}
 
 defRecord :: String -> String -> A.Type -> State CompState ()
-defRecord rec mem t = defineName (simpleName rec) $ A.NameDef emptyMeta rec rec (A.RecordType emptyMeta False [(simpleName mem,t)]) A.Original A.Unplaced
+defRecord rec mem t = defineName (simpleName rec) $
+  A.NameDef emptyMeta rec rec
+    (A.RecordType emptyMeta False [(simpleName mem,t)])
+    A.Original A.NameUser A.Unplaced
 
 testGenVariable :: Test
 testGenVariable = TestList
@@ -827,7 +830,9 @@ testGenVariable = TestList
      ,testBothS ("testGenVariable/unchecked" ++ show n) eUC eUCPP (over (tcall genVariableUnchecked $ sub $ A.Variable emptyMeta foo)) state
     ]
      where
-       state = do defineName (simpleName "foo") $ A.NameDef emptyMeta "foo" "foo" (A.Declaration emptyMeta t) am A.Unplaced
+       state = do defineName (simpleName "foo") $
+                    A.NameDef emptyMeta "foo" "foo"
+                      (A.Declaration emptyMeta t) am A.NameUser A.Unplaced
                   defRecord "bar" "x" $ A.Array [dimension 7] A.Int
                   defRecord "barbar" "y" $ A.Record bar
        over :: Override
diff --git a/common/OccamEDSL.hs b/common/OccamEDSL.hs
index d74e119..336597d 100644
--- a/common/OccamEDSL.hs
+++ b/common/OccamEDSL.hs
@@ -22,7 +22,7 @@ module OccamEDSL (ExpInp, ExpInpT,
   oCASE, oCASEinput, caseOption, inputCaseOption, 
   oALT, guard,
   oIF, ifChoice,
-  Occ, oA, oB, oC, oX, oY, oZ, p0, p1, p2, (*?), (*!), (*:=), (*+), decl, decl', decl'',
+  Occ, oA, oB, oC, oX, oY, oZ, p0, p1, p2, (*?), (*!), (*:=), (*+), decl, declNonce, decl',
     sub,
     oempty, testOccamPass,
     oprocess,
@@ -307,18 +307,20 @@ decl bty bvar scope = do
   return $ A.Spec emptyMeta (A.Specification emptyMeta name $ A.Declaration emptyMeta ty)
     (singlify $ A.Several emptyMeta s)
 
-decl' :: Data a => A.Name -> A.SpecType ->
+declNonce :: Data a => ExpInp A.Type -> ExpInp A.Variable ->
   [O (A.Structured a)] -> O (A.Structured a)
-decl' n sp scope = do
-  defineThing (A.nameName n) sp A.Original
+declNonce bty bvar scope = do
+  ty <- liftExpInp bty
+  (A.Variable _ name) <- liftExpInp bvar
+  defineThing (A.nameName name) (A.Declaration emptyMeta ty) A.Original A.NameNonce
   s <- sequence scope
-  return $ A.Spec emptyMeta (A.Specification emptyMeta n sp)
+  return $ A.Spec emptyMeta (A.Specification emptyMeta name $ A.Declaration emptyMeta ty)
     (singlify $ A.Several emptyMeta s)
 
-decl'' :: Data a => A.Name -> A.SpecType -> A.AbbrevMode ->
+decl' :: Data a => A.Name -> A.SpecType -> A.AbbrevMode -> A.NameSource ->
   [O (A.Structured a)] -> O (A.Structured a)
-decl'' n sp am scope = do
-  defineThing (A.nameName n) sp am
+decl' n sp am ns scope = do
+  defineThing (A.nameName n) sp am ns
   s <- sequence scope
   return $ A.Spec emptyMeta (A.Specification emptyMeta n sp)
     (singlify $ A.Several emptyMeta s)
diff --git a/common/TestUtils.hs b/common/TestUtils.hs
index 3296680..87b596f 100644
--- a/common/TestUtils.hs
+++ b/common/TestUtils.hs
@@ -294,6 +294,7 @@ buildExpr (Func f es) = A.FunctionCall emptyMeta (simpleName f) (map buildExpr e
 -- | A simple definition of a variable
 simpleDef :: String -> A.SpecType -> A.NameDef
 simpleDef n sp = A.NameDef {A.ndMeta = emptyMeta, A.ndName = n, A.ndOrigName = n,
+                            A.ndNameSource = A.NameUser,
                             A.ndSpecType = sp, A.ndAbbrevMode = A.Original, A.ndPlacement = A.Unplaced}
 
 -- | A simple definition of a declared variable
@@ -308,14 +309,15 @@ simpleDefPattern n am sp = tag6 A.NameDef DontCare n n sp am A.Unplaced
 --{{{  defining things
 
 -- | Define something in the initial state.
-defineThing :: CSM m => String -> A.SpecType -> A.AbbrevMode -> m ()
-defineThing s st am = defineName (simpleName s) $
+defineThing :: CSM m => String -> A.SpecType -> A.AbbrevMode -> A.NameSource -> m ()
+defineThing s st am ns = defineName (simpleName s) $
     A.NameDef {
       A.ndMeta = emptyMeta,
       A.ndName = s,
       A.ndOrigName = s,
       A.ndSpecType = st,
       A.ndAbbrevMode = am,
+      A.ndNameSource = ns,
       A.ndPlacement = A.Unplaced
     }
 
@@ -323,17 +325,17 @@ defineThing s st am = defineName (simpleName s) $
 defineConst :: String -> A.Type -> A.Expression -> State CompState ()
 defineConst s t e
     = defineThing s (A.IsExpr emptyMeta A.ValAbbrev t e)
-                  A.ValAbbrev
+                  A.ValAbbrev A.NameUser
 
 -- | Define an @IS@ abbreviation.
 defineIs :: String -> A.Type -> A.Variable -> State CompState ()
 defineIs s t v
-    = defineThing s (A.Is emptyMeta A.Abbrev t v) A.Abbrev
+    = defineThing s (A.Is emptyMeta A.Abbrev t v) A.Abbrev A.NameUser
 
 -- | Define something original.
 defineOriginal :: CSM m => String -> A.Type -> m ()
 defineOriginal s t
-    = defineThing s (A.Declaration emptyMeta t) A.Original
+    = defineThing s (A.Declaration emptyMeta t) A.Original A.NameUser
 
 -- | Define a variable.
 defineVariable :: CSM m => String -> A.Type -> m ()
@@ -350,13 +352,13 @@ defineTimer = defineOriginal
 -- | Define a user data type.
 defineUserDataType :: String -> A.Type -> State CompState ()
 defineUserDataType s t
-    = defineThing s (A.DataType emptyMeta t) A.Original
+    = defineThing s (A.DataType emptyMeta t) A.Original A.NameUser
 
 -- | Define a record type.
 -- (The fields are unscoped names, and thus don't need defining.)
 defineRecordType :: String -> [(String, A.Type)] -> State CompState ()
 defineRecordType s fs
-    = defineThing s st A.Original
+    = defineThing s st A.Original A.NameUser
   where
     st = A.RecordType emptyMeta False [(simpleName s, t) | (s, t) <- fs]
 
@@ -364,7 +366,7 @@ defineRecordType s fs
 defineFunction :: String -> [A.Type] -> [(String, A.Type)]
                   -> State CompState ()
 defineFunction s rs as
-    = defineThing s st A.Original
+    = defineThing s st A.Original A.NameUser
   where
     st = A.Function emptyMeta A.PlainSpec rs fs (Right $ A.Skip emptyMeta)
     fs = [A.Formal A.ValAbbrev t (simpleName s) | (s, t) <- as]
@@ -372,7 +374,7 @@ defineFunction s rs as
 -- | Define a proc.
 defineProc :: CSM m => String -> [(String, A.AbbrevMode, A.Type)] -> m ()
 defineProc s as
-    = defineThing s st A.Original
+    = defineThing s st A.Original A.NameUser
   where
     st = A.Proc emptyMeta A.PlainSpec fs $ A.Skip emptyMeta
     fs = [A.Formal am t (simpleName s) | (s, am, t) <- as]
@@ -380,12 +382,12 @@ defineProc s as
 -- | Define a protocol.
 defineProtocol :: String -> [A.Type] -> State CompState ()
 defineProtocol s ts
-    = defineThing s (A.Protocol emptyMeta ts) A.Original
+    = defineThing s (A.Protocol emptyMeta ts) A.Original A.NameUser
 
 -- | Define a variant protocol.
 defineProtocolCase :: String -> [(A.Name, [A.Type])] -> State CompState ()
 defineProtocolCase s ntss
-    = defineThing s (A.ProtocolCase emptyMeta ntss) A.Original
+    = defineThing s (A.ProtocolCase emptyMeta ntss) A.Original A.NameUser
 
 --}}}
 --{{{  custom assertions
diff --git a/data/AST.hs b/data/AST.hs
index 821912a..ad400e0 100644
--- a/data/AST.hs
+++ b/data/AST.hs
@@ -61,11 +61,19 @@ data NameDef = NameDef {
     ndSpecType :: SpecType,
     -- | The abbreviation mode of the name's definition (see 'AbbrevMode').
     ndAbbrevMode :: AbbrevMode,
+    -- | The source of the name (see 'NameSource').
+    ndNameSource :: NameSource,
     -- | The placement mode of the name's definition (see 'Placement').
     ndPlacement :: Placement
   }
   deriving (Show, Eq, Typeable, Data)
 
+data NameSource
+  = NameUser       -- ^ A name from the source program
+  | NameNonce      -- ^ A name the compiler generated
+  | NamePredefined -- ^ A magic name without definition (e.g. the Rain timer)
+  deriving (Show, Eq, Typeable, Data)
+
 -- | The direction of a channel.
 data Direction =
   DirInput         -- ^ The input end.
diff --git a/data/CompState.hs b/data/CompState.hs
index 8957c70..44372a5 100644
--- a/data/CompState.hs
+++ b/data/CompState.hs
@@ -113,7 +113,6 @@ data CompState = CompState {
     csMainLocals :: [(String, (A.Name, NameType))],
     csNames :: Map String A.NameDef,
     csUnscopedNames :: Map String String,
-    csGhostNames :: Set A.Name,
     csNameCounter :: Int,
 
     -- Set by passes
@@ -155,7 +154,6 @@ emptyState = CompState {
     csMainLocals = [],
     csNames = Map.empty,
     csUnscopedNames = Map.empty,
-    csGhostNames = Set.empty,
     csNameCounter = 0,
 
     csTypeContext = [],
@@ -214,12 +212,6 @@ defineName :: CSM m => A.Name -> A.NameDef -> m ()
 defineName n nd
     = modify $ (\ps -> ps { csNames = Map.insert (A.nameName n) nd (csNames ps) })
 
--- | Add the definition of a ghost name.
-defineGhostName :: CSM m => A.Name -> A.NameDef -> m ()
-defineGhostName n nd
-    =  do defineName n nd
-          modify (\cs -> cs { csGhostNames = Set.insert n (csGhostNames cs) })
-
 -- | Modify the definition of a name.
 modifyName :: CSM m => A.Name -> (A.NameDef -> A.NameDef) -> m ()
 modifyName n f
@@ -238,6 +230,9 @@ lookupNameOrError n err
             Just nd -> return nd
             Nothing -> err
 
+nameSource :: (CSMR m, Die m) => A.Name -> m A.NameSource
+nameSource n = lookupName n >>* A.ndNameSource
+
 -- | Make a name unique by appending a suffix to it.
 makeUniqueName :: CSM m => String -> m String
 makeUniqueName s
@@ -260,17 +255,12 @@ findUnscopedName n@(A.Name m s)
                                     , A.ndOrigName = s
                                     , A.ndSpecType = A.Unscoped m
                                     , A.ndAbbrevMode = A.Original
+                                    , A.ndNameSource = A.NameUser
                                     , A.ndPlacement = A.Unplaced
                                     }
                  defineName n nd
                  return n
 
--- | Determine whether a name is a ghost name.
-isGhostName :: CSMR m => A.Name -> m Bool
-isGhostName n
-    =  do ghostNames <- getCompState >>* csGhostNames
-          return $ n `Set.member` ghostNames
-
 --}}}
 
 --{{{  pulled items
@@ -350,6 +340,7 @@ defineNonce m s st am
                      A.ndOrigName = ns,
                      A.ndSpecType = st,
                      A.ndAbbrevMode = am,
+                     A.ndNameSource = A.NameNonce,
                      A.ndPlacement = A.Unplaced
                    }
           defineName n nd
diff --git a/frontends/ParseOccam.hs b/frontends/ParseOccam.hs
index 226d4c4..69182fd 100644
--- a/frontends/ParseOccam.hs
+++ b/frontends/ParseOccam.hs
@@ -368,6 +368,7 @@ scopeIn n@(A.Name m s) nt specType am
             A.ndOrigName = s,
             A.ndSpecType = specType,
             A.ndAbbrevMode = am,
+            A.ndNameSource = A.NameUser,
             A.ndPlacement = A.Unplaced
           }
           defineName n' nd
diff --git a/frontends/ParseRain.hs b/frontends/ParseRain.hs
index ddbf3fa..a6ab4c2 100644
--- a/frontends/ParseRain.hs
+++ b/frontends/ParseRain.hs
@@ -526,6 +526,7 @@ rainTimerNameDef
                 , A.ndOrigName = A.nameName rainTimerName
                 , A.ndSpecType = A.Declaration emptyMeta (A.Timer A.RainTimer)
                 , A.ndAbbrevMode = A.Original
+                , A.ndNameSource = A.NamePredefined
                 , A.ndPlacement = A.Unplaced
                 }
 
@@ -536,7 +537,7 @@ parseRainProgram filename source
           case lexOut of
             Left merr -> dieP merr $ "Parse (lexing) error"
             Right toks ->
-              do defineGhostName rainTimerName rainTimerNameDef
+              do defineName rainTimerName rainTimerNameDef
                  cs <- get
                  case runParser rainSourceFile cs filename toks of
                    Left err -> dieP (sourcePosToMeta $ errorPos err) $ "Parse error: " ++ show err
diff --git a/frontends/RainPasses.hs b/frontends/RainPasses.hs
index 5009767..0755a6e 100644
--- a/frontends/RainPasses.hs
+++ b/frontends/RainPasses.hs
@@ -91,7 +91,7 @@ uniquifyAndResolveVars = rainOnlyPass
       = do (params',procBody') <- doFormals params procBody
            let newProc = (A.Proc m'' procMode params' procBody')
            defineName n A.NameDef {A.ndMeta = m', A.ndName = A.nameName n, A.ndOrigName = A.nameName n,
-                                   A.ndSpecType = newProc, 
+                                   A.ndSpecType = newProc, A.ndNameSource = A.NameUser,
                                    A.ndAbbrevMode = A.Original, A.ndPlacement = A.Unplaced}
            return $ A.Spec m (A.Specification m' n newProc) scope
     -- Functions:
@@ -100,7 +100,7 @@ uniquifyAndResolveVars = rainOnlyPass
       = do (params', funcBody') <- doFormals params funcBody
            let newFunc = (A.Function m'' funcMode retTypes params' funcBody')
            defineName n A.NameDef {A.ndMeta = m', A.ndName = A.nameName n, A.ndOrigName = A.nameName n,
-                                   A.ndSpecType = newFunc,
+                                   A.ndSpecType = newFunc, A.ndNameSource = A.NameUser,
                                    A.ndAbbrevMode = A.Original, A.ndPlacement = A.Unplaced}
            return $ A.Spec m (A.Specification m' n newFunc) scope
 
@@ -108,7 +108,7 @@ uniquifyAndResolveVars = rainOnlyPass
     uniquifyAndResolveVars' (A.Spec m (A.Specification m' n decl) scope) 
       = do n' <- makeNonce $ A.nameName n
            defineName (n {A.nameName = n'}) A.NameDef {A.ndMeta = m', A.ndName = n', A.ndOrigName = A.nameName n, 
-                                                       A.ndSpecType = decl, 
+                                                       A.ndSpecType = decl, A.ndNameSource = A.NameUser,
                                                        A.ndAbbrevMode = A.Original, A.ndPlacement = A.Unplaced}
            let scope' = everywhere (mkT $ replaceNameName (A.nameName n) n') scope
            return $ A.Spec m (A.Specification m' n {A.nameName = n'} decl) scope'
@@ -131,6 +131,7 @@ uniquifyAndResolveVars = rainOnlyPass
            let m = A.nameMeta n
            defineName newName A.NameDef {A.ndMeta = m, A.ndName = n', A.ndOrigName = A.nameName n, 
                                          A.ndSpecType = (A.Declaration m t),
+                                         A.ndNameSource = A.NameUser,
                                          A.ndAbbrevMode = am, A.ndPlacement = A.Unplaced}
            let scope' = everywhere (mkT $ replaceNameName (A.nameName n) n') scope
            return (A.Formal am t newName, scope')
diff --git a/frontends/RainPassesTest.hs b/frontends/RainPassesTest.hs
index 99a0d29..575c699 100644
--- a/frontends/RainPassesTest.hs
+++ b/frontends/RainPassesTest.hs
@@ -122,7 +122,8 @@ testUnique0 = TestCase $ testPassWithItemsStateCheck "testUnique0" exp uniquifyA
       = do newcName <- castAssertADI (Map.lookup "newc" items)
            assertNotEqual "testUnique0: Variable was not made unique" "c" (A.nameName newcName)
            assertVarDef "testUnique0: Variable was not recorded" state (A.nameName newcName)
-             (tag6 A.NameDef DontCare (A.nameName newcName) "c" (A.Declaration m A.Byte) A.Original A.Unplaced)
+             (tag7 A.NameDef DontCare (A.nameName newcName) "c"
+               (A.Declaration m A.Byte) A.Original A.NameUser A.Unplaced)
 
 -- | Tests that two declarations of a variable with the same name are indeed made unique:
 testUnique1 :: Test
@@ -139,9 +140,11 @@ testUnique1 = TestCase $ testPassWithItemsStateCheck "testUnique1" exp uniquifyA
                      assertNotEqual "testUnique1: Variable was not made unique" "c" (A.nameName newc1Name)
                      assertNotEqual "testUnique1: Variables were not made unique" (A.nameName newc0Name) (A.nameName newc1Name)
                      assertVarDef "testUnique1: Variable was not recorded" state (A.nameName newc0Name)
-                       (tag6 A.NameDef DontCare (A.nameName newc0Name) "c" (A.Declaration m A.Byte ) A.Original A.Unplaced)
+                       (tag7 A.NameDef DontCare (A.nameName newc0Name) "c"
+                         (A.Declaration m A.Byte) A.Original A.NameUser A.Unplaced)
                      assertVarDef "testUnique1: Variable was not recorded" state (A.nameName newc1Name)
-                       (tag6 A.NameDef DontCare (A.nameName newc1Name) "c" (A.Declaration m A.Int64 ) A.Original A.Unplaced)
+                       (tag7 A.NameDef DontCare (A.nameName newc1Name) "c"
+                         (A.Declaration m A.Int64) A.Original A.NameUser A.Unplaced)
 
 -- | Tests that the unique pass does resolve the variables that are in scope
 testUnique2 :: Test
@@ -175,7 +178,8 @@ testUnique3 = TestCase $ testPassWithItemsStateCheck "testUnique3" exp uniquifyA
     orig = A.Spec m (A.Specification m (procName "foo") $ A.Proc m A.PlainSpec [] $ A.Skip m) (A.Only m $ A.ProcCall m (procName "foo") [])
     exp = orig
     check (items,state) = assertVarDef "testUnique3: Variable was not recorded" state "foo"
-                            (tag6 A.NameDef DontCare "foo" "foo" (A.Proc m A.PlainSpec [] $ A.Skip m) A.Original A.Unplaced)
+                            (tag7 A.NameDef DontCare "foo" "foo"
+                              (A.Proc m A.PlainSpec [] $ A.Skip m) A.Original A.NameUser A.Unplaced)
 
 -- | Tests that parameters are uniquified and resolved:
 testUnique4 :: Test
@@ -198,10 +202,13 @@ testUnique4 = TestCase $ testPassWithItemsStateCheck "testUnique4" exp uniquifyA
       = do newcName <- castAssertADI (Map.lookup "newc" items)
            assertNotEqual "testUnique4: Variable was not made unique" "c" (A.nameName newcName)
            assertVarDef "testUnique4: Variable was not recorded" state (A.nameName newcName)
-             (tag6 A.NameDef DontCare (A.nameName newcName) "c" (A.Declaration m A.Byte ) A.ValAbbrev A.Unplaced)
+             (tag7 A.NameDef DontCare (A.nameName newcName) "c"
+               (A.Declaration m A.Byte) A.ValAbbrev A.NameUser A.Unplaced)
            assertVarDef "testUnique4: Variable was not recorded" state "foo"
-             (tag6 A.NameDef DontCare "foo" "foo" (tag4 A.Proc DontCare A.PlainSpec 
-               [tag3 A.Formal A.ValAbbrev A.Byte newcName] (bodyPattern newcName)) A.Original A.Unplaced)
+             (tag7 A.NameDef DontCare "foo" "foo"
+               (tag4 A.Proc DontCare A.PlainSpec 
+                 [tag3 A.Formal A.ValAbbrev A.Byte newcName] (bodyPattern newcName))
+               A.Original A.NameUser A.Unplaced)
            
 -- TODO check that doing {int : c; { int: c; } } does give an error
 -- TODO check that declaring a new proc with the same name as an old one does give an error
@@ -227,7 +234,7 @@ testFindMain0 = TestCase $ testPassWithItemsStateCheck "testFindMain0" exp (uniq
            assertNotEqual "testFindMain0 A" "main" mainName
            assertEqual "testFindMain0 B" [(mainName, (A.Name m mainName, ProcName))] (csMainLocals state)
            assertVarDef "testFindMain0 C" state mainName
-                       (tag6 A.NameDef DontCare mainName "main" DontCare A.Original A.Unplaced)
+                       (tag7 A.NameDef DontCare mainName "main" DontCare A.Original A.NameUser A.Unplaced)
 
 testFindMain1 :: Test
 testFindMain1 = TestCase $ testPassWithStateCheck "testFindMain1" orig (uniquifyAndResolveVars >>> findMain) orig (return ()) check
diff --git a/pass/PassList.hs b/pass/PassList.hs
index d93291f..202d6ad 100644
--- a/pass/PassList.hs
+++ b/pass/PassList.hs
@@ -82,12 +82,12 @@ nullStateBodies = Pass
   ,passEnabled = const True}
   where
     nullProcFuncDefs :: A.NameDef -> A.NameDef
-    nullProcFuncDefs (A.NameDef m n on (A.Proc m' sm fs _) am pl)
-      = (A.NameDef m n on (A.Proc m' sm fs (A.Skip m')) am pl)
-    nullProcFuncDefs (A.NameDef m n on (A.Function m' sm ts fs (Left _)) am pl)
-      = (A.NameDef m n on (A.Function m' sm ts fs (Left $ A.Several m' [])) am pl)
-    nullProcFuncDefs (A.NameDef m n on (A.Function m' sm ts fs (Right _)) am pl)
-      = (A.NameDef m n on (A.Function m' sm ts fs (Right $ A.Skip m')) am pl)
+    nullProcFuncDefs (A.NameDef m n on (A.Proc m' sm fs _) am ns pl)
+      = (A.NameDef m n on (A.Proc m' sm fs (A.Skip m')) am ns pl)
+    nullProcFuncDefs (A.NameDef m n on (A.Function m' sm ts fs (Left _)) am ns pl)
+      = (A.NameDef m n on (A.Function m' sm ts fs (Left $ A.Several m' [])) am ns pl)
+    nullProcFuncDefs (A.NameDef m n on (A.Function m' sm ts fs (Right _)) am ns pl)
+      = (A.NameDef m n on (A.Function m' sm ts fs (Right $ A.Skip m')) am ns pl)
     nullProcFuncDefs x = x
     
 
diff --git a/transformations/PassTest.hs b/transformations/PassTest.hs
index 5068ead..f4e19c7 100644
--- a/transformations/PassTest.hs
+++ b/transformations/PassTest.hs
@@ -84,10 +84,12 @@ testFunctionsToProcs0 = TestCase $ testPassWithItemsStateCheck "testFunctionsToP
                              --check return parameters were defined:
     check (items,state) = do ret0 <- ((assertGetItemCast "ret0" items) :: IO A.Name)                        
                              assertVarDef "testFunctionsToProcs0" state (A.nameName ret0) $
-                               tag6 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0) (A.Declaration m A.Int) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0)
+                                 (A.Declaration m A.Int) A.Abbrev A.NameNonce A.Unplaced
                              --check proc was defined:
                              assertVarDef "testFunctionsToProcs0" state "foo" $
-                               tag6 A.NameDef DontCare ("foo") ("foo") procSpec A.Original A.Unplaced
+                               tag7 A.NameDef DontCare ("foo") ("foo")
+                                 procSpec A.Original A.NameUser A.Unplaced
                              --check csFunctionReturns was changed:
                              assertEqual "testFunctionsToProcs0" (Just [A.Int]) (Map.lookup "foo" (csFunctionReturns state)) 
 
@@ -110,12 +112,15 @@ testFunctionsToProcs1 = TestCase $ testPassWithItemsStateCheck "testFunctionsToP
     check (items,state) = do ret0 <- ((assertGetItemCast "ret0" items) :: IO A.Name)
                              ret1 <- ((assertGetItemCast "ret1" items) :: IO A.Name)
                              assertVarDef "testFunctionsToProcs1 B" state (A.nameName ret0) $
-                               tag6 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0) (A.Declaration m A.Int) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0)
+                                 (A.Declaration m A.Int) A.Abbrev A.NameNonce A.Unplaced
                              assertVarDef "testFunctionsToProcs1 C" state (A.nameName ret1) $
-                               tag6 A.NameDef DontCare (A.nameName ret1) (A.nameName ret1) (A.Declaration m A.Real32) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName ret1) (A.nameName ret1)
+                                 (A.Declaration m A.Real32) A.Abbrev A.NameNonce A.Unplaced
                              --check proc was defined:
                              assertVarDef "testFunctionsToProcs1 D" state "foo" $
-                               tag6 A.NameDef DontCare ("foo") ("foo") procBody A.Original A.Unplaced
+                               tag7 A.NameDef DontCare ("foo") ("foo")
+                                 procBody A.Original A.NameUser A.Unplaced
                              --check csFunctionReturns was changed:
                              assertEqual "testFunctionsToProcs1 E" (Just [A.Int,A.Real32]) (Map.lookup "foo" (csFunctionReturns state)) 
 
@@ -140,14 +145,18 @@ testFunctionsToProcs2 = TestCase $ testPassWithItemsStateCheck "testFunctionsToP
     check (items,state) = do retOuter0 <- ((assertGetItemCast "retOuter0" items) :: IO A.Name)
                              ret0 <- ((assertGetItemCast "ret0" items) :: IO A.Name)
                              assertVarDef "testFunctionsToProcs2 B" state (A.nameName ret0) $
-                               tag6 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0) (A.Declaration m A.Int) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0)
+                                 (A.Declaration m A.Int) A.Abbrev A.NameNonce A.Unplaced
                              assertVarDef "testFunctionsToProcs2 C" state (A.nameName retOuter0) $
-                               tag6 A.NameDef DontCare (A.nameName retOuter0) (A.nameName retOuter0) (A.Declaration m A.Int) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName retOuter0) (A.nameName retOuter0)
+                                 (A.Declaration m A.Int) A.Abbrev A.NameNonce A.Unplaced
                              --check proc was defined:
                              assertVarDef "testFunctionsToProcs2 D" state "foo" $
-                               tag6 A.NameDef DontCare ("foo") ("foo") (singleParamSpecExp DontCare) A.Original A.Unplaced
+                               tag7 A.NameDef DontCare ("foo") ("foo") (singleParamSpecExp DontCare)
+                                 A.Original A.NameUser A.Unplaced
                              assertVarDef "testFunctionsToProcs2 E" state "fooOuter" $
-                               tag6 A.NameDef DontCare ("fooOuter") ("fooOuter") (procHeader DontCare) A.Original A.Unplaced
+                               tag7 A.NameDef DontCare ("fooOuter") ("fooOuter") (procHeader DontCare)
+                                 A.Original A.NameUser A.Unplaced
                              --check csFunctionReturns was changed:
                              assertEqual "testFunctionsToProcs2 F" (Just [A.Int]) (Map.lookup "foo" (csFunctionReturns state)) 
                              assertEqual "testFunctionsToProcs2 G" (Just [A.Int]) (Map.lookup "fooOuter" (csFunctionReturns state)) 
@@ -162,10 +171,12 @@ testFunctionsToProcs3 = TestCase $ testPassWithItemsStateCheck "testFunctionsToP
                              --check return parameters were defined:
     check (items,state) = do ret0 <- ((assertGetItemCast "ret0" items) :: IO A.Name)                        
                              assertVarDef "testFunctionsToProcs3" state (A.nameName ret0) $
-                               tag6 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0) (A.Declaration m A.Int) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0)
+                                 (A.Declaration m A.Int) A.Abbrev A.NameNonce A.Unplaced
                              --check proc was defined:
                              assertVarDef "testFunctionsToProcs3" state "foo" $
-                               tag6 A.NameDef DontCare ("foo") ("foo") procSpec A.Original A.Unplaced
+                               tag7 A.NameDef DontCare ("foo") ("foo")
+                                 procSpec A.Original A.NameUser A.Unplaced
                              --check csFunctionReturns was changed:
                              assertEqual "testFunctionsToProcs3" (Just [A.Int]) (Map.lookup "foo" (csFunctionReturns state)) 
 
@@ -189,12 +200,15 @@ testFunctionsToProcs4 = TestCase $ testPassWithItemsStateCheck "testFunctionsToP
     check (items,state) = do ret0 <- ((assertGetItemCast "ret0" items) :: IO A.Name)
                              ret1 <- ((assertGetItemCast "ret1" items) :: IO A.Name)
                              assertVarDef "testFunctionsToProcs4 B" state (A.nameName ret0) $
-                               tag6 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0) (A.Declaration m A.Int) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName ret0) (A.nameName ret0)
+                                 (A.Declaration m A.Int) A.Abbrev A.NameNonce A.Unplaced
                              assertVarDef "testFunctionsToProcs4 C" state (A.nameName ret1) $
-                               tag6 A.NameDef DontCare (A.nameName ret1) (A.nameName ret1) (A.Declaration m A.Real32) A.Abbrev A.Unplaced
+                               tag7 A.NameDef DontCare (A.nameName ret1) (A.nameName ret1)
+                                 (A.Declaration m A.Real32) A.Abbrev A.NameNonce A.Unplaced
                              --check proc was defined:
                              assertVarDef "testFunctionsToProcs4 D" state "foo" $
-                               tag6 A.NameDef DontCare ("foo") ("foo") procBody A.Original A.Unplaced
+                               tag7 A.NameDef DontCare ("foo") ("foo")
+                                 procBody A.Original A.NameUser A.Unplaced
                              --check csFunctionReturns was changed:
                              assertEqual "testFunctionsToProcs4 E" (Just [A.Int,A.Real32]) (Map.lookup "foo" (csFunctionReturns state)) 
 
@@ -354,7 +368,7 @@ testInputCase = TestList
        )
        `becomes`
        oSEQ
-          [decl (return A.Int) oA
+          [declNonce (return A.Int) oA
             [oC *? oA
             ,oCASE oA
               [caseOption ([0 :: Int], p0)]
@@ -399,7 +413,7 @@ testInputCase = TestList
        )
        `becomes`
        oSEQ
-          [decl (return A.Int) oA
+          [declNonce (return A.Int) oA
             [oC *? oA
             ,oCASE oA
               [caseOption ([0 :: Int], p0)
@@ -459,7 +473,7 @@ testInputCase = TestList
        )
        `becomes`
        oSEQ
-          [decl (return A.Int) oA
+          [declNonce (return A.Int) oA
             [oC *? oA
             ,oCASE oA
               [caseOption ([0 :: Int], p0)
@@ -500,7 +514,7 @@ testInputCase = TestList
        )
        `becomes`
        oALT
-          [decl (return A.Int) oA
+          [declNonce (return A.Int) oA
             [guard (oC *? oA,
               oCASE oA
                 [caseOption ([0 :: Int], p0)])
@@ -515,9 +529,11 @@ testInputCase = TestList
 
     defineProtocolAndC :: Occ (A.Structured A.Process) -> Occ (A.Structured A.Process)
     defineProtocolAndC =
-      decl' (simpleName "prot") (A.ProtocolCase emptyMeta [(a0,[]),(b2,[A.Int,A.Int]),(c1,[A.Int])])
-      . (:[]) . decl (return $ A.Chan A.DirUnknown (A.ChanAttributes False False) (A.UserProtocol $ simpleName "prot"))
-          oC . (:[])
+      decl' (simpleName "prot")
+        (A.ProtocolCase emptyMeta [(a0,[]),(b2,[A.Int,A.Int]),(c1,[A.Int])])
+          A.Original A.NameUser
+          . singleton . decl (return $ A.Chan A.DirUnknown (A.ChanAttributes False False)
+                               (A.UserProtocol $ simpleName "prot")) oC . singleton
     
 testTransformProtocolInput :: Test
 testTransformProtocolInput = TestList
@@ -571,15 +587,15 @@ testPullRepCounts = TestList
       (blockType
         [decl' (simpleName "X")
           (A.Rep emptyMeta (A.For emptyMeta (intLiteral 0) (intLiteral 6)))
-            []
+            A.Original A.NameUser []
         ]
       `becomes`
        blockType
-        [decl'' (simpleName "A")
-          (A.IsExpr emptyMeta A.ValAbbrev A.Int $ intLiteral 6) A.ValAbbrev
+        [decl' (simpleName "A")
+          (A.IsExpr emptyMeta A.ValAbbrev A.Int $ intLiteral 6) A.ValAbbrev A.NameNonce
           [decl' (simpleName "X")
             (A.Rep emptyMeta (A.For emptyMeta (intLiteral 0) (exprVariable "A")))
-              []
+              A.Original A.NameUser []
           ]
         ]
       ) pullRepCounts 
@@ -589,21 +605,24 @@ testPullRepCounts = TestList
        (blockType
          [decl' (simpleName "X")
           (A.Rep emptyMeta (A.For emptyMeta (intLiteral 0) (intLiteral 6)))
+          A.Original A.NameUser
             [decl' (simpleName "Y")
               (A.Rep emptyMeta (A.For emptyMeta (intLiteral 1) (intLiteral 8)))
-                []
+                A.Original A.NameUser []
             ]
          ]
        `becomes`
        blockType
-         [decl'' (simpleName "A")
-          (A.IsExpr emptyMeta A.ValAbbrev A.Int $ intLiteral 6) A.ValAbbrev
+         [decl' (simpleName "A")
+          (A.IsExpr emptyMeta A.ValAbbrev A.Int $ intLiteral 6) A.ValAbbrev A.NameNonce
            [decl' (simpleName "X")
             (A.Rep emptyMeta (A.For emptyMeta (intLiteral 0) (exprVariable "A")))
-              [decl'' (simpleName "B")
-                (A.IsExpr emptyMeta A.ValAbbrev A.Int $ intLiteral 8) A.ValAbbrev
+              A.Original A.NameUser
+              [decl' (simpleName "B")
+                (A.IsExpr emptyMeta A.ValAbbrev A.Int $ intLiteral 8) A.ValAbbrev A.NameNonce
                   [decl' (simpleName "Y")
                     (A.Rep emptyMeta (A.For emptyMeta (intLiteral 1) (exprVariable "B")))
+                      A.Original A.NameUser
                       []
                   ]
               ]
diff --git a/transformations/SimplifyExprs.hs b/transformations/SimplifyExprs.hs
index 3855c4c..f122d14 100644
--- a/transformations/SimplifyExprs.hs
+++ b/transformations/SimplifyExprs.hs
@@ -70,6 +70,7 @@ functionsToProcs = pass "Convert FUNCTIONs to PROCs"
                         A.ndOrigName = A.nameName n,
                         A.ndSpecType = st,
                         A.ndAbbrevMode = A.Original,
+                        A.ndNameSource = A.NameUser,
                         A.ndPlacement = A.Unplaced
                       }
              defineName n nd
diff --git a/transformations/Unnest.hs b/transformations/Unnest.hs
index faaca3b..d26bd6e 100644
--- a/transformations/Unnest.hs
+++ b/transformations/Unnest.hs
@@ -150,8 +150,8 @@ removeFreeNames = pass "Convert free names to arguments"
     isFreeName n
         =  do st <- specTypeOfName n
               isConst <- isConstantName n
-              isGhost <- isGhostName n
-              return $ isFreeST st && not (isConst || isGhost)
+              src <- nameSource n
+              return $ isFreeST st && not (isConst || src == A.NamePredefined)
       where
         isFreeST :: A.SpecType -> Bool
         isFreeST st