diff --git a/saw-core/src/Verifier/SAW/Grammar.y b/saw-core/src/Verifier/SAW/Grammar.y
index 293f494041..498f2a1065 100644
--- a/saw-core/src/Verifier/SAW/Grammar.y
+++ b/saw-core/src/Verifier/SAW/Grammar.y
@@ -26,6 +26,7 @@ import Control.Monad.State (State, get, gets, modify, put, runState, evalState)
 import Control.Monad.Except (ExceptT, throwError, runExceptT)
 import qualified Data.ByteString.Lazy.UTF8 as B
 import Data.Maybe (isJust)
+import Data.Text (Text)
 import qualified Data.Text as Text
 import Data.Traversable
 import Data.Word
@@ -171,12 +172,12 @@ AppTerm : AtomTerm                 { $1 }
 AtomTerm :: { Term }
 AtomTerm
   : nat                          { NatLit (pos $1) (tokNat (val $1)) }
-  | string                       { StringLit (pos $1) (tokString (val $1)) }
+  | string                       { StringLit (pos $1) (Text.pack (tokString (val $1))) }
   | Ident                        { Name $1 }
   | IdentRec                     { Recursor Nothing $1 }
   | 'Prop'                       { Sort (pos $1) propSort }
   | 'sort' nat                   { Sort (pos $1) (mkSort (tokNat (val $2))) }
-  | AtomTerm '.' Ident           { RecordProj $1 (Text.pack (val $3)) }
+  | AtomTerm '.' Ident           { RecordProj $1 (val $3) }
   | AtomTerm '.' IdentRec        {% parseRecursorProj $1 $3 }
   | AtomTerm '.' nat             {% parseTupleSelector $1 (fmap tokNat $3) }
   | '(' sepBy(Term, ',') ')'     { mkTupleValue (pos $1) $2 }
@@ -186,17 +187,17 @@ AtomTerm
   | '#' '{' sepBy(FieldType, ',') '}'  { RecordType  (pos $1) $3 }
   | AtomTerm '.' '(' nat ')'           {% mkTupleProj $1 (tokNat (val $4)) }
 
-Ident :: { PosPair String }
-Ident : ident { fmap tokIdent $1 }
+Ident :: { PosPair Text }
+Ident : ident { fmap (Text.pack . tokIdent) $1 }
 
-IdentRec :: { PosPair String }
-IdentRec : identrec { fmap tokRecursor $1 }
+IdentRec :: { PosPair Text }
+IdentRec : identrec { fmap (Text.pack . tokRecursor) $1 }
 
 FieldValue :: { (PosPair FieldName, Term) }
-FieldValue : Ident '=' Term { (fmap Text.pack $1, $3) }
+FieldValue : Ident '=' Term { ($1, $3) }
 
 FieldType :: { (PosPair FieldName, Term) }
-FieldType : Ident ':' LTerm { (fmap Text.pack $1, $3) }
+FieldType : Ident ':' LTerm { ($1, $3) }
 
 opt(q) :: { Maybe q }
   : { Nothing }
@@ -341,7 +342,7 @@ parseModuleName (RecordProj t str) = (++ [Text.unpack str]) <$> parseModuleName
 parseModuleName _ = Nothing
 
 -- | Parse a qualified recursor @M1.M2...Mn.d#rec@
-parseRecursorProj :: Term -> PosPair String -> Parser Term
+parseRecursorProj :: Term -> PosPair Text -> Parser Term
 parseRecursorProj (parseModuleName -> Just mnm) i =
   return $ Recursor (Just $ mkModuleName mnm) i
 parseRecursorProj t _ =
@@ -356,9 +357,9 @@ parseTupleSelector t i =
 
 -- | Create a module name given a list of strings with the top-most
 -- module name given first.
-mkPosModuleName :: [PosPair String] -> PosPair ModuleName
+mkPosModuleName :: [PosPair Text] -> PosPair ModuleName
 mkPosModuleName [] = error "internal: Unexpected empty module name"
-mkPosModuleName l = PosPair p (mkModuleName nms)
+mkPosModuleName l = PosPair p (mkModuleName (fmap Text.unpack nms))
   where nms = fmap val l
         p = pos (last l)
 }
diff --git a/saw-core/src/Verifier/SAW/Module.hs b/saw-core/src/Verifier/SAW/Module.hs
index ae1d815eb1..f8d476507e 100644
--- a/saw-core/src/Verifier/SAW/Module.hs
+++ b/saw-core/src/Verifier/SAW/Module.hs
@@ -80,6 +80,7 @@ import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.HashMap.Strict (HashMap)
 import qualified Data.HashMap.Strict as HMap
+import Data.Text (Text)
 import GHC.Generics (Generic)
 
 import qualified Language.Haskell.TH.Syntax as TH
@@ -232,7 +233,7 @@ instance Show DataType where
 data ModuleDecl = TypeDecl DataType
                 | DefDecl Def
 
--- | The different sorts of things that a 'String' name can be resolved to
+-- | The different sorts of things that a 'Text' name can be resolved to
 data ResolvedName
   = ResolvedCtor Ctor
   | ResolvedDataType DataType
@@ -245,14 +246,14 @@ resolvedNameIdent (ResolvedDataType dt) = dtName dt
 resolvedNameIdent (ResolvedDef d) = defIdent d
 
 -- | Modules define namespaces of datatypes, constructors, and definitions,
--- i.e., mappings from 'String' names to these objects. A module is allowed to
--- map a 'String' name to an object defined in a different module. Modules also
+-- i.e., mappings from 'Text' names to these objects. A module is allowed to
+-- map a 'Text' name to an object defined in a different module. Modules also
 -- keep a record of the top-level declarations and the imports that were used to
 -- build them.
 data Module = Module {
           moduleName    :: !ModuleName
         , moduleImports :: !(Map ModuleName Module)
-        , moduleResolveMap :: !(Map String ResolvedName)
+        , moduleResolveMap :: !(Map Text ResolvedName)
         , moduleRDecls   :: [ModuleDecl] -- ^ All declarations in reverse order they were added.
         }
 
@@ -269,35 +270,35 @@ emptyModule nm =
          }
 
 
--- | Resolve a 'String' name in the namespace defined by a 'Module', to either a
+-- | Resolve a 'Text' name in the namespace defined by a 'Module', to either a
 -- 'Ctor', 'DataType', or 'Def'
-resolveName :: Module -> String -> Maybe ResolvedName
+resolveName :: Module -> Text -> Maybe ResolvedName
 resolveName m str = Map.lookup str (moduleResolveMap m)
 
--- | Resolve a 'String' name to a 'Ctor'
-findCtor :: Module -> String -> Maybe Ctor
+-- | Resolve a 'Text' name to a 'Ctor'
+findCtor :: Module -> Text -> Maybe Ctor
 findCtor m str =
   resolveName m str >>= \case { ResolvedCtor ctor -> Just ctor; _ -> Nothing }
 
--- | Resolve a 'String' name to a 'DataType'
-findDataType :: Module -> String -> Maybe DataType
+-- | Resolve a 'Text' name to a 'DataType'
+findDataType :: Module -> Text -> Maybe DataType
 findDataType m str =
   resolveName m str >>= \case { ResolvedDataType d -> Just d; _ -> Nothing }
 
--- | Resolve a 'String' name to a 'Def'
-findDef :: Module -> String -> Maybe Def
+-- | Resolve a 'Text' name to a 'Def'
+findDef :: Module -> Text -> Maybe Def
 findDef m str =
   resolveName m str >>= \case { ResolvedDef d -> Just d; _ -> Nothing }
 
 
--- | Insert a 'ResolvedName' into a 'Module', adding a mapping from the 'String'
+-- | Insert a 'ResolvedName' into a 'Module', adding a mapping from the 'Text'
 -- name of that resolved name to it. Signal an error in the case of a name
--- clash, i.e., an existing binding for the same 'String' name.
+-- clash, i.e., an existing binding for the same 'Text' name.
 insResolvedName :: Module -> ResolvedName -> Module
 insResolvedName m nm =
-  let str = identName $ resolvedNameIdent nm in
+  let str = identBaseName $ resolvedNameIdent nm in
   if Map.member str (moduleResolveMap m) then
-    internalError ("Duplicate name " ++ str ++ " being inserted into module "
+    internalError ("Duplicate name " ++ show str ++ " being inserted into module "
                    ++ show (moduleName m))
   else
     m { moduleResolveMap = Map.insert str nm (moduleResolveMap m) }
@@ -329,7 +330,7 @@ beginDataType m dt =
 
 -- | Complete a datatype, by adding its constructors
 completeDataType :: Module -> Ident -> [Ctor] -> Module
-completeDataType m (identName -> str) ctors =
+completeDataType m (identBaseName -> str) ctors =
   case resolveName m str of
     Just (ResolvedDataType dt)
       | null (dtCtors dt) ->
@@ -339,11 +340,11 @@ completeDataType m (identName -> str) ctors =
               Map.insert str (ResolvedDataType dt') (moduleResolveMap m),
               moduleRDecls = TypeDecl dt' : moduleRDecls m }
     Just (ResolvedDataType _) ->
-      internalError $ "completeDataType: datatype already completed: " ++ str
+      internalError $ "completeDataType: datatype already completed: " ++ show str
     Just _ ->
-      internalError $ "completeDataType: not a datatype: " ++ str
+      internalError $ "completeDataType: not a datatype: " ++ show str
     Nothing ->
-      internalError $ "completeDataType: datatype not found: " ++ str
+      internalError $ "completeDataType: datatype not found: " ++ show str
 
 
 -- | Insert a definition into a module
@@ -413,12 +414,12 @@ type ModuleMap = HashMap ModuleName Module
 -- | Resolve an 'Ident' to a 'Ctor' in a 'ModuleMap'
 findCtorInMap :: ModuleMap -> Ident -> Maybe Ctor
 findCtorInMap m i =
-  HMap.lookup (identModule i) m >>= flip findCtor (identName i)
+  HMap.lookup (identModule i) m >>= flip findCtor (identBaseName i)
 
 -- | Resolve an 'Ident' to a 'DataType' in a 'ModuleMap'
 findDataTypeInMap :: ModuleMap -> Ident -> Maybe DataType
 findDataTypeInMap m i =
-  HMap.lookup (identModule i) m >>= flip findDataType (identName i)
+  HMap.lookup (identModule i) m >>= flip findDataType (identBaseName i)
 
 -- | Get all definitions defined in any module in an entire module map. Note
 -- that the returned list might have redundancies if a definition is visible /
diff --git a/saw-core/src/Verifier/SAW/Name.hs b/saw-core/src/Verifier/SAW/Name.hs
index 291cda154a..c2961e6e91 100644
--- a/saw-core/src/Verifier/SAW/Name.hs
+++ b/saw-core/src/Verifier/SAW/Name.hs
@@ -25,6 +25,7 @@ module Verifier.SAW.Name
   , moduleNamePieces
    -- * Identifiers
   , Ident(identModule, identBaseName), identName, mkIdent
+  , mkIdentText
   , parseIdent
   , isIdent
   , identText
@@ -133,6 +134,9 @@ instance Read Ident where
 mkIdent :: ModuleName -> String -> Ident
 mkIdent m s = Ident m (Text.pack s)
 
+mkIdentText :: ModuleName -> Text -> Ident
+mkIdentText m s = Ident m s
+
 -- | Parse a fully qualified identifier.
 parseIdent :: String -> Ident
 parseIdent s0 =
diff --git a/saw-core/src/Verifier/SAW/ParserUtils.hs b/saw-core/src/Verifier/SAW/ParserUtils.hs
index c3ac50ada0..f30eab06e9 100644
--- a/saw-core/src/Verifier/SAW/ParserUtils.hs
+++ b/saw-core/src/Verifier/SAW/ParserUtils.hs
@@ -32,6 +32,8 @@ import qualified Data.ByteString.Lazy as BL
 #if !MIN_VERSION_template_haskell(2,8,0)
 import qualified Data.ByteString.Lazy.UTF8 as UTF8
 #endif
+import Data.Text (Text)
+import qualified Data.Text as Text
 import Language.Haskell.TH
 #if MIN_VERSION_template_haskell(2,7,0)
 import Language.Haskell.TH.Syntax (qAddDependentFile)
@@ -135,13 +137,13 @@ declareTermApplyFun nm n tf =
 --
 -- The number of 'Term's to take as arguments is given by the arity of @tp@,
 -- i.e., the number of nested pi-abstractions it contains at top level.
-declareTypedNameFun :: Q Exp -> ModuleName -> String -> Bool -> Un.Term ->
+declareTypedNameFun :: Q Exp -> ModuleName -> Text -> Bool -> Un.Term ->
                        DecWriter ()
 declareTypedNameFun sc_fun mnm nm apply_p tp =
-  let th_nm = (if apply_p then "scApply" else "sc") ++ show mnm ++ "_" ++ nm in
+  let th_nm = (if apply_p then "scApply" else "sc") ++ show mnm ++ "_" ++ Text.unpack nm in
   declareTermApplyFun th_nm (length $ fst $ Un.asPiList tp) $ \sc ts ->
   [| $(sc_fun) $(varE sc)
-   (mkIdent mnm $(stringE nm))
+   (mkIdent mnm $(stringE (Text.unpack nm)))
    $(ts) |]
 
 -- | Declare a Haskell function
@@ -150,7 +152,7 @@ declareTypedNameFun sc_fun mnm nm apply_p tp =
 --
 -- for declared name (primitive, axiom, or definition) @d@ with type @tp@ in
 -- module @MMM@
-declareDefFun :: ModuleName -> String -> Un.Term -> DecWriter ()
+declareDefFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
 declareDefFun mnm d tp =
   declareTypedNameFun [| scGlobalApply |] mnm d True tp
 
@@ -159,7 +161,7 @@ declareDefFun mnm d tp =
 -- > scMMM_d :: SharedContext -> Term -> ... -> Term -> IO Term
 --
 -- for datatype @d@ with parameters @p_ctx@ and type @tp@ in module @MMM@
-declareDataTypeFun :: ModuleName -> String -> Un.Term -> DecWriter ()
+declareDataTypeFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
 declareDataTypeFun mnm d tp =
   declareTypedNameFun [| scDataTypeApp |] mnm d False tp
 
@@ -168,7 +170,7 @@ declareDataTypeFun mnm d tp =
 -- > scApplyMMM_c :: SharedContext -> Term -> ... -> Term -> IO Term
 --
 -- for constructor @c@ with type (including parameters) @tp@ in module @MMM@
-declareCtorFun :: ModuleName -> String -> Un.Term -> DecWriter ()
+declareCtorFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
 declareCtorFun mnm c tp =
   declareTypedNameFun [| scCtorApp |] mnm c True tp
 
diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs
index 422511b607..bd786f0686 100644
--- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs
+++ b/saw-core/src/Verifier/SAW/SCTypeCheck.hs
@@ -49,6 +49,7 @@ import Control.Monad.Reader
 import Data.List ( (\\) )
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Text (Text)
 #if !MIN_VERSION_base(4,8,0)
 import Data.Traversable (Traversable(..))
 #endif
@@ -148,7 +149,7 @@ data TCError
   | NotRecordType TypedTerm
   | BadRecordField FieldName Term
   | DanglingVar Int
-  | UnboundName String
+  | UnboundName Text
   | SubtypeFailure TypedTerm Term
   | EmptyVectorLit
   | NoSuchDataType Ident
@@ -157,7 +158,7 @@ data TCError
   | BadParamsOrArgsLength Bool Ident [Term] [Term]
   | BadConstType NameInfo Term Term
   | MalformedRecursor Term String
-  | DeclError String String
+  | DeclError Text String
   | ErrorPos Pos TCError
   | ErrorCtx LocalName Term TCError
 
@@ -202,7 +203,7 @@ prettyTCError e = runReader (helper e) ([], Nothing) where
                 , ishow ty ]
   helper (DanglingVar n) =
       ppWithPos [ return ("Dangling bound variable index: " ++ show n)]
-  helper (UnboundName str) = ppWithPos [ return ("Unbound name: " ++ str)]
+  helper (UnboundName str) = ppWithPos [ return ("Unbound name: " ++ show str)]
   helper (SubtypeFailure trm tp2) =
       ppWithPos [ return "Inferred type", ishow (typedType trm),
                   return "Not a subtype of expected type", ishow tp2,
@@ -228,7 +229,7 @@ prettyTCError e = runReader (helper e) ([], Nothing) where
       ppWithPos [ return "Malformed recursor application",
                   ishow trm, return reason ]
   helper (DeclError nm reason) =
-    ppWithPos [ return ("Malformed declaration for " ++ nm), return reason ]
+    ppWithPos [ return ("Malformed declaration for " ++ show nm), return reason ]
   helper (ErrorPos p err) =
     local (\(ctx,_) -> (ctx, Just p)) $ helper err
   helper (ErrorCtx x _ err) =
diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index f5dbe0f8fc..f1ae46d393 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -510,7 +510,7 @@ scFindModule sc name =
 -- | Look up a definition by its identifier
 scFindDef :: SharedContext -> Ident -> IO (Maybe Def)
 scFindDef sc i =
-  findDef <$> scFindModule sc (identModule i) <*> return (identName i)
+  findDef <$> scFindModule sc (identModule i) <*> pure (identBaseName i)
 
 -- | Look up a 'Def' by its identifier, throwing an error if it is not found
 scRequireDef :: SharedContext -> Ident -> IO Def
@@ -523,7 +523,7 @@ scRequireDef sc i =
 -- | Look up a datatype by its identifier
 scFindDataType :: SharedContext -> Ident -> IO (Maybe DataType)
 scFindDataType sc i =
-  findDataType <$> scFindModule sc (identModule i) <*> return (identName i)
+  findDataType <$> scFindModule sc (identModule i) <*> pure (identBaseName i)
 
 -- | Look up a datatype by its identifier, throwing an error if it is not found
 scRequireDataType :: SharedContext -> Ident -> IO DataType
@@ -536,7 +536,7 @@ scRequireDataType sc i =
 -- | Look up a constructor by its identifier
 scFindCtor :: SharedContext -> Ident -> IO (Maybe Ctor)
 scFindCtor sc i =
-  findCtor <$> scFindModule sc (identModule i) <*> return (identName i)
+  findCtor <$> scFindModule sc (identModule i) <*> pure (identBaseName i)
 
 -- | Look up a constructor by its identifier, throwing an error if not found
 scRequireCtor :: SharedContext -> Ident -> IO Ctor
diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs
index 0cce4600c1..6028f08a81 100644
--- a/saw-core/src/Verifier/SAW/Typechecker.hs
+++ b/saw-core/src/Verifier/SAW/Typechecker.hs
@@ -35,7 +35,7 @@ import Control.Applicative
 #endif
 import Control.Monad.State
 import Data.List (findIndex)
-import qualified Data.Text as Text
+import Data.Text (Text)
 import qualified Data.Vector as V
 
 import Prettyprinter hiding (Doc)
@@ -43,6 +43,7 @@ import Prettyprinter hiding (Doc)
 import Verifier.SAW.Utils (internalError)
 
 import Verifier.SAW.Module
+import Verifier.SAW.Name (mkIdentText)
 import Verifier.SAW.Position
 import Verifier.SAW.Term.Functor
 import Verifier.SAW.Term.CtxTerm
@@ -93,11 +94,11 @@ inferApplyAll t (arg:args) =
      inferApplyAll app1 args
 
 -- | Resolve a name in the current module and apply it to some arguments
-inferResolveNameApp :: String -> [TypedTerm] -> TCM TypedTerm
+inferResolveNameApp :: Text -> [TypedTerm] -> TCM TypedTerm
 inferResolveNameApp n args =
   do ctx <- askCtx
      m <- getModule
-     case (findIndex ((== Text.pack n) . fst) ctx, resolveName m n) of
+     case (findIndex ((== n) . fst) ctx, resolveName m n) of
        (Just i, _) ->
          do t <- typeInferComplete (LocalVar i :: TermF TypedTerm)
             inferApplyAll t args
@@ -119,7 +120,7 @@ inferResolveNameApp n args =
          throwTCError $ UnboundName n
 
 -- | Match an untyped term as a name applied to 0 or more arguments
-matchAppliedName :: Un.Term -> Maybe (String, [Un.Term])
+matchAppliedName :: Un.Term -> Maybe (Text, [Un.Term])
 matchAppliedName (Un.Name (PosPair _ n)) = Just (n, [])
 matchAppliedName (Un.App f arg) =
   do (n, args) <- matchAppliedName f
@@ -127,7 +128,7 @@ matchAppliedName (Un.App f arg) =
 matchAppliedName _ = Nothing
 
 -- | Match an untyped term as a recursor applied to 0 or more arguments
-matchAppliedRecursor :: Un.Term -> Maybe (Maybe ModuleName, String, [Un.Term])
+matchAppliedRecursor :: Un.Term -> Maybe (Maybe ModuleName, Text, [Un.Term])
 matchAppliedRecursor (Un.Recursor mnm (PosPair _ n)) = Just (mnm, n, [])
 matchAppliedRecursor (Un.App f arg) =
   do (mnm, n, args) <- matchAppliedRecursor f
@@ -177,7 +178,7 @@ typeInferCompleteTerm (matchAppliedRecursor -> Just (maybe_mnm, str, args)) =
          Just mnm -> return mnm
          Nothing -> getModuleName
      m <- liftTCM scFindModule mnm
-     let dt_ident = mkIdent mnm str
+     let dt_ident = mkIdentText mnm str
      dt <- case findDataType m str of
        Just d -> return d
        Nothing -> throwTCError $ NoSuchDataType dt_ident
@@ -264,7 +265,7 @@ typeInferCompleteTerm (Un.TypeConstraint t _ tp) =
 typeInferCompleteTerm (Un.NatLit _ i) =
   typeInferComplete (NatLit i :: FlatTermF TypedTerm)
 typeInferCompleteTerm (Un.StringLit _ str) =
-  typeInferComplete (StringLit (Text.pack str) :: FlatTermF TypedTerm)
+  typeInferComplete (StringLit str :: FlatTermF TypedTerm)
 typeInferCompleteTerm (Un.VecLit _ []) = throwTCError EmptyVectorLit
 typeInferCompleteTerm (Un.VecLit _ ts) =
   do typed_ts <- mapM typeInferComplete ts
@@ -329,7 +330,7 @@ processDecls (Un.TypeDecl NoQualifier (PosPair p nm) tp :
 
      -- Step 4: add the definition to the current module
      mnm <- getModuleName
-     let ident = mkIdent mnm nm
+     let ident = mkIdentText mnm nm
      t <- liftTCM scConstant' (ModuleIdentifier ident) def_tm def_tp
      liftTCM scRegisterGlobal ident t
      liftTCM scModifyModule mnm $ \m ->
@@ -349,7 +350,7 @@ processDecls (Un.TypeDecl q (PosPair p nm) tp : rest) =
    do typed_tp <- typeInferComplete tp
       void $ ensureSort $ typedType typed_tp
       mnm <- getModuleName
-      let ident = mkIdent mnm nm
+      let ident = mkIdentText mnm nm
       let nmi = ModuleIdentifier ident
       i <- liftTCM scFreshGlobalVar
       liftTCM scRegisterName i nmi
@@ -405,7 +406,7 @@ processDecls (Un.DataDecl (PosPair p nm) param_ctx dt_tp c_decls : rest) =
 
   -- Step 4: Add d as an empty datatype, so we can typecheck the constructors
   mnm <- getModuleName
-  let dtName = mkIdent mnm nm
+  let dtName = mkIdentText mnm nm
   let dt = DataType { dtCtors = [], .. }
   liftTCM scModifyModule mnm (\m -> beginDataType m dt)
 
@@ -421,10 +422,10 @@ processDecls (Un.DataDecl (PosPair p nm) param_ctx dt_tp c_decls : rest) =
             forM typed_ctors $ \(c, tp) ->
             case mkCtorArgStruct dtName p_ctx ix_ctx tp of
               Just arg_struct ->
-                liftTCM scBuildCtor dtName (mkIdent mnm c)
-                (map (mkIdent mnm . fst) typed_ctors)
+                liftTCM scBuildCtor dtName (mkIdentText mnm c)
+                (map (mkIdentText mnm . fst) typed_ctors)
                 arg_struct
-              Nothing -> err ("Malformed type form constructor: " ++ c)
+              Nothing -> err ("Malformed type form constructor: " ++ show c)
 
   -- Step 6: complete the datatype with the given ctors
   liftTCM scModifyModule mnm (\m -> completeDataType m dtName ctors)
diff --git a/saw-core/src/Verifier/SAW/UntypedAST.hs b/saw-core/src/Verifier/SAW/UntypedAST.hs
index 29356a3ac4..47134b3afc 100644
--- a/saw-core/src/Verifier/SAW/UntypedAST.hs
+++ b/saw-core/src/Verifier/SAW/UntypedAST.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TupleSections #-}
 
 {- |
@@ -45,6 +46,7 @@ module Verifier.SAW.UntypedAST
 #if !MIN_VERSION_base(4,8,0)
 import Control.Applicative ((<$>))
 #endif
+import Data.Text (Text)
 import qualified Data.Text as Text
 
 import qualified Language.Haskell.TH.Syntax as TH
@@ -59,12 +61,12 @@ import Verifier.SAW.TypedAST
   )
 
 data Term
-  = Name (PosPair String)
+  = Name (PosPair Text)
   | Sort Pos Sort
   | App Term Term
   | Lambda Pos TermCtx Term
   | Pi Pos TermCtx Term
-  | Recursor (Maybe ModuleName) (PosPair String)
+  | Recursor (Maybe ModuleName) (PosPair Text)
   | UnitValue Pos
   | UnitType Pos
     -- | New-style records
@@ -79,7 +81,7 @@ data Term
     -- | Identifies a type constraint on the term, i.e., a type ascription
   | TypeConstraint Term Pos Term
   | NatLit Pos Natural
-  | StringLit Pos String
+  | StringLit Pos Text
     -- | Vector literal.
   | VecLit Pos [Term]
   | BadTerm Pos
@@ -87,19 +89,19 @@ data Term
 
 -- | A pattern used for matching a variable.
 data TermVar
-  = TermVar (PosPair String)
+  = TermVar (PosPair LocalName)
   | UnusedVar Pos
   deriving (Eq, Ord, Show, TH.Lift)
 
 -- | Return the 'String' name associated with a 'TermVar'
 termVarString :: TermVar -> String
-termVarString (TermVar (PosPair _ str)) = str
+termVarString (TermVar (PosPair _ str)) = Text.unpack str
 termVarString (UnusedVar _) = "_"
 
 -- | Return the 'LocalName' associated with a 'TermVar'
 termVarLocalName :: TermVar -> LocalName
-termVarLocalName (TermVar (PosPair _ str)) = Text.pack str
-termVarLocalName (UnusedVar _) = Text.pack "_"
+termVarLocalName (TermVar (PosPair _ str)) = str
+termVarLocalName (UnusedVar _) = "_"
 
 -- | A context of 0 or more variable bindings, with types
 type TermCtx = [(TermVar,Term)]
@@ -136,20 +138,20 @@ badTerm :: Pos -> Term
 badTerm = BadTerm
 
 -- | A constructor declaration of the form @c (x1 :: tp1) .. (xn :: tpn) :: tp@
-data CtorDecl = Ctor (PosPair String) TermCtx Term
+data CtorDecl = Ctor (PosPair Text) TermCtx Term
   deriving (Show, TH.Lift)
 
 -- | A top-level declaration in a saw-core file
 data Decl
-   = TypeDecl DefQualifier (PosPair String) Term
+   = TypeDecl DefQualifier (PosPair Text) Term
      -- ^ A declaration of something having a type, where the declaration
      -- qualifier states what flavor of thing it is
-   | DataDecl (PosPair String) TermCtx Term [CtorDecl]
+   | DataDecl (PosPair Text) TermCtx Term [CtorDecl]
      -- ^ A declaration of an inductive data types, with a name, a parameter
      -- context, a return type, and a list of constructor declarations
-   | TermDef (PosPair String) [TermVar] Term
+   | TermDef (PosPair Text) [TermVar] Term
      -- ^ A declaration of a term having a definition, with variables
-   | TypedDef (PosPair String) [(TermVar, Term)] Term Term
+   | TypedDef (PosPair Text) [(TermVar, Term)] Term Term
      -- ^ A definition of something with a specific type, with parameters
   deriving (Show, TH.Lift)
 
@@ -188,20 +190,20 @@ moduleName (Module (PosPair _ mnm) _ _) = mnm
 
 -- | Get a list of all names (i.e., definitions, axioms, or primitives) declared
 -- in a module, along with their types and qualifiers
-moduleTypedDecls :: Module -> [(String, Term)]
+moduleTypedDecls :: Module -> [(Text, Term)]
 moduleTypedDecls (Module _ _ decls) = concatMap helper decls where
-  helper :: Decl -> [(String, Term)]
+  helper :: Decl -> [(Text, Term)]
   helper (TypeDecl _ (PosPair _ nm) tm) = [(nm,tm)]
   helper _ = []
 
 -- | Get a list of all datatypes declared in a module
-moduleDataDecls :: Module -> [(String,TermCtx,Term,[CtorDecl])]
+moduleDataDecls :: Module -> [(Text, TermCtx, Term, [CtorDecl])]
 moduleDataDecls (Module _ _ decls) = concatMap helper decls where
-  helper :: Decl -> [(String,TermCtx,Term,[CtorDecl])]
+  helper :: Decl -> [(Text, TermCtx, Term, [CtorDecl])]
   helper (DataDecl (PosPair _ nm) params tp ctors) = [(nm, params, tp, ctors)]
   helper _ = []
 
-moduleTypedDataDecls :: Module -> [(String,Term)]
+moduleTypedDataDecls :: Module -> [(Text, Term)]
 moduleTypedDataDecls =
   map (\(nm,p_ctx,tp,_) ->
         (nm, Pi (pos tp) p_ctx tp)) . moduleDataDecls
@@ -213,7 +215,7 @@ moduleCtorDecls =
   concatMap (\(_,p_ctx,_,ctors) -> map (p_ctx,) ctors) . moduleDataDecls
 
 -- | Get a list of the names and types of all the constructors in a module
-moduleTypedCtorDecls :: Module -> [(String,Term)]
+moduleTypedCtorDecls :: Module -> [(Text, Term)]
 moduleTypedCtorDecls =
   concatMap (\(_,p_ctx,_,ctors) ->
               map (\(Ctor (PosPair _ nm) ctx tp) ->