diff --git a/src/Verifier/SAW/ExternalFormat.hs b/src/Verifier/SAW/ExternalFormat.hs
index 654efbff..670fe1e7 100644
--- a/src/Verifier/SAW/ExternalFormat.hs
+++ b/src/Verifier/SAW/ExternalFormat.hs
@@ -87,11 +87,6 @@ scWriteExternal t0 =
             PairType x y        -> unwords ["PairT", show x, show y]
             PairLeft e          -> unwords ["ProjL", show e]
             PairRight e         -> unwords ["ProjR", show e]
-            EmptyValue          -> unwords ["Empty"]
-            EmptyType           -> unwords ["EmptyT"]
-            FieldValue f x y    -> unwords ["OldRecord", show f, show x, show y]
-            FieldType f x y     -> unwords ["OldRecordT", show f, show x, show y]
-            RecordSelector e i  -> unwords ["OldRecordSel", show e, show i]
             CtorApp i ps es     ->
               unwords ("Ctor" : show i : map show ps ++ argsep : map show es)
             DataTypeApp i ps es ->
@@ -142,11 +137,6 @@ scReadExternal sc input =
         ["PairT", x, y]     -> FTermF (PairType (read x) (read y))
         ["ProjL", x]        -> FTermF (PairLeft (read x))
         ["ProjR", x]        -> FTermF (PairRight (read x))
-        ["Empty"]           -> FTermF EmptyValue
-        ["EmptyT"]          -> FTermF EmptyType
-        ["OldRecord",f,x,y] -> FTermF (FieldValue (read f) (read x) (read y))
-        ["OldRecordT",f,x,y] -> FTermF (FieldType (read f) (read x) (read y))
-        ["OldRecordSel", e, i] -> FTermF (RecordSelector (read e) (read i))
         ("Ctor" : i : (separateArgs -> Just (ps, es))) ->
           FTermF (CtorApp (parseIdent i) (map read ps) (map read es))
         ("Data" : i : (separateArgs -> Just (ps, es))) ->
diff --git a/src/Verifier/SAW/Recognizer.hs b/src/Verifier/SAW/Recognizer.hs
index bd889c8b..4d55c94a 100644
--- a/src/Verifier/SAW/Recognizer.hs
+++ b/src/Verifier/SAW/Recognizer.hs
@@ -31,14 +31,9 @@ module Verifier.SAW.Recognizer
   , asTupleType
   , asTupleValue
   , asTupleSelector
-  , asFieldType
-  , asFieldValue
   , asRecordType
   , asRecordValue
   , asRecordSelector
-  , asOldRecordType
-  , asOldRecordValue
-  , asOldRecordSelector
   , asCtorParams
   , asCtor
   , asCtorOrNat
@@ -203,20 +198,6 @@ asTupleSelector t = do
     PairRight y -> do (x, i) <- asTupleSelector y; return (x, i+1)
     _           -> fail "asTupleSelector"
 
-asFieldType :: (Monad m) => Recognizer m Term (Term, Term, Term)
-asFieldType t = do
-  ftf <- asFTermF t
-  case ftf of
-    FieldType x y z -> return (x, y, z)
-    _               -> fail "asFieldType"
-
-asFieldValue :: (Monad m) => Recognizer m Term (Term, Term, Term)
-asFieldValue t = do
-  ftf <- asFTermF t
-  case ftf of
-    FieldValue x y z -> return (x, y, z)
-    _                -> fail "asFieldValue"
-
 asRecordType :: (Monad m) => Recognizer m Term (Map FieldName Term)
 asRecordType t = do
   ftf <- asFTermF t
@@ -224,18 +205,6 @@ asRecordType t = do
     RecordType elems -> return $ Map.fromList elems
     _                -> fail $ "asRecordType: " ++ showTerm t
 
--- | Old version of 'asRecordType', that works on old-style record types
-asOldRecordType :: (Monad m) => Recognizer m Term (Map FieldName Term)
-asOldRecordType t = do
-  ftf <- asFTermF t
-  case ftf of
-    EmptyType       -> return Map.empty
-    FieldType f x y -> do m <- asRecordType y
-                          s <- asStringLit f
-                          return (Map.insert s x m)
-    _               -> fail $ "asRecordType: " ++ showTerm t
-
-
 asRecordValue :: (Monad m) => Recognizer m Term (Map FieldName Term)
 asRecordValue t = do
   ftf <- asFTermF t
@@ -243,28 +212,11 @@ asRecordValue t = do
     RecordValue elems -> return $ Map.fromList elems
     _                 -> fail $ "asRecordValue: " ++ showTerm t
 
--- | Old version of 'asRecordValue', that uses 'EmptyValue' and 'FieldValue'
-asOldRecordValue :: (Monad m) => Recognizer m Term (Map FieldName Term)
-asOldRecordValue t = do
-  ftf <- asFTermF t
-  case ftf of
-    EmptyValue       -> return Map.empty
-    FieldValue f x y -> do m <- asRecordValue y
-                           s <- asStringLit f
-                           return (Map.insert s x m)
-    _                -> fail $ "asRecordValue: " ++ showTerm t
-
 asRecordSelector :: (Monad m) => Recognizer m Term (Term, FieldName)
 asRecordSelector t = do
   RecordProj u s <- asFTermF t
   return (u, s)
 
-asOldRecordSelector :: (Monad m) => Recognizer m Term (Term, FieldName)
-asOldRecordSelector t = do
-  RecordSelector u i <- asFTermF t
-  s <- asStringLit i
-  return (u, s)
-
 -- | Test whether a term is an application of a constructor, and, if so, return
 -- the constructor, its parameters, and its arguments
 asCtorParams :: (Monad f) => Recognizer f Term (Ident, [Term], [Term])
diff --git a/src/Verifier/SAW/Rewriter.hs b/src/Verifier/SAW/Rewriter.hs
index da5ce897..48c7a600 100644
--- a/src/Verifier/SAW/Rewriter.hs
+++ b/src/Verifier/SAW/Rewriter.hs
@@ -588,11 +588,6 @@ rewriteSharedTermTypeSafe sc ss t0 =
           PairType{}       -> return ftf -- doesn't matter
           PairLeft{}       -> traverse rewriteAll ftf
           PairRight{}      -> traverse rewriteAll ftf
-          EmptyValue       -> return ftf
-          EmptyType        -> return ftf
-          FieldValue{}     -> traverse rewriteAll ftf
-          FieldType{}      -> return ftf -- doesn't matter
-          RecordSelector{} -> traverse rewriteAll ftf
 
           -- NOTE: we don't rewrite arguments of constructors, datatypes, or
           -- recursors because of dependent types, as we could potentially cause
diff --git a/src/Verifier/SAW/SCTypeCheck.hs b/src/Verifier/SAW/SCTypeCheck.hs
index 5380a3e0..3a00fafd 100644
--- a/src/Verifier/SAW/SCTypeCheck.hs
+++ b/src/Verifier/SAW/SCTypeCheck.hs
@@ -398,16 +398,6 @@ instance TypeInfer (FlatTermF TypedTerm) where
     do sx <- ensureSort tx
        sy <- ensureSort ty
        liftTCM scSort (max sx sy)
-  typeInfer EmptyValue = liftTCM scEmptyType
-  typeInfer EmptyType = liftTCM scSort (mkSort 0)
-  typeInfer (FieldValue f (TypedTerm _ tx) (TypedTerm _ ty)) =
-    do checkField f
-       liftTCM scFieldType (typedVal f) tx ty
-  typeInfer (FieldType f (TypedTerm _ tx) (TypedTerm _ ty)) =
-    do checkField f
-       sx <- ensureSort tx
-       sy <- ensureSort ty
-       liftTCM scSort (max sx sy)
   typeInfer (PairLeft (TypedTerm _ tp)) =
     case asPairType tp of
       Just (t1, _) -> typeCheckWHNF t1
@@ -416,18 +406,6 @@ instance TypeInfer (FlatTermF TypedTerm) where
     case asPairType tp of
       Just (_, t2) -> typeCheckWHNF t2
       _ -> throwTCError (NotTupleType tp)
-  typeInfer (RecordSelector t@(TypedTerm _ tp) f@(TypedTerm f_trm _)) =
-    do checkField f
-       maybe_str <- asStringLit <$> typeCheckWHNF f_trm
-       f_str <- case maybe_str of
-         Just x -> return x
-         Nothing -> throwTCError (NotStringLit f_trm)
-       case asRecordType tp of
-         Just m ->
-           case Map.lookup f_str m of
-             Nothing -> throwTCError $ BadRecordField f_str tp
-             Just f_tp -> typeCheckWHNF f_tp
-         _ -> throwTCError (NotRecordType t)
 
   typeInfer (DataTypeApp d params args) =
     -- Look up the DataType structure, check the length of the params and args,
@@ -543,12 +521,6 @@ isSubtype t1' t2' = areConvertible t1' t2'
 areConvertible :: Term -> Term -> TCM Bool
 areConvertible t1 t2 = liftTCM scConvertibleEval scTypeCheckWHNF True t1 t2
 
--- | Check that a term has type @String@
-checkField :: TypedTerm -> TCM ()
-checkField t =
-  do string_tp <- liftTCM scStringType
-     checkSubtype t string_tp
-
 -- | Infer the type of a recursor application
 inferRecursorApp :: Ident -> [TypedTerm] -> TypedTerm ->
                     [(Ident,TypedTerm)] -> [TypedTerm] -> TypedTerm ->
diff --git a/src/Verifier/SAW/SharedTerm.hs b/src/Verifier/SAW/SharedTerm.hs
index d90cb13f..aece2d62 100644
--- a/src/Verifier/SAW/SharedTerm.hs
+++ b/src/Verifier/SAW/SharedTerm.hs
@@ -79,9 +79,6 @@ module Verifier.SAW.SharedTerm
   , scRecord
   , scRecordSelect
   , scRecordType
-  , scOldRecord
-  , scOldRecordSelect
-  , scOldRecordType
   , scDataTypeAppParams
   , scDataTypeApp
   , scCtorAppParams
@@ -122,10 +119,6 @@ module Verifier.SAW.SharedTerm
   , scPairType
   , scPairLeft
   , scPairRight
-  , scEmptyValue
-  , scEmptyType
-  , scFieldValue
-  , scFieldType
   , scTuple
   , scTupleType
   , scTupleSelector
@@ -581,7 +574,6 @@ data WHNFElim
   = ElimApp Term
   | ElimProj String
   | ElimPair Bool
-  | ElimOldProj FieldName
   | ElimRecursor Ident [Term] Term [(Ident,Term)] [Term]
 
 -- | Test if a term is a constructor application that should be converted to a
@@ -620,7 +612,6 @@ scWhnf sc t0 =
     go xs                     (convertsToNat    -> Just k) = scFlatTermF sc (NatLit k) >>= go xs
     go xs                     (asApp            -> Just (t, x)) = go (ElimApp x : xs) t
     go xs                     (asRecordSelector -> Just (t, n)) = go (ElimProj n : xs) t
-    go xs                     (asOldRecordSelector -> Just (t, n)) = go (ElimOldProj n : xs) t
     go xs                     (asPairSelector -> Just (t, i)) = go (ElimPair i : xs) t
     go (ElimApp x : xs)       (asLambda -> Just (_, _, body))   = instantiateVar sc 0 x body >>= go xs
     go (ElimPair i : xs)      (asPairValue -> Just (a, b))      = go xs (if i then b else a)
@@ -628,12 +619,6 @@ scWhnf sc t0 =
                                                                     Just t -> go xs t
                                                                     Nothing ->
                                                                       error "scWhnf: field missing in record"
-    go (ElimOldProj i : xs)   (asFieldValue -> Just (s, a, b))  = do s' <- memo s
-                                                                     b' <- memo b
-                                                                     t' <- scFieldValue sc s' a b'
-                                                                     case asRecordValue t' of
-                                                                       Just tm -> go xs ((Map.!) tm i)
-                                                                       Nothing -> foldM reapply t' xs
     go (ElimRecursor d ps
         p_ret cs_fs _ : xs)   (asCtorOrNat ->
                                Just (c, _, args))               = (scReduceRecursor sc d ps
@@ -646,19 +631,10 @@ scWhnf sc t0 =
     go xs                     (asPairValue -> Just (a, b))      = do b' <- memo b
                                                                      t' <- scPairValue sc a b'
                                                                      foldM reapply t' xs
-    go xs                     (asFieldValue -> Just (s, a, b))  = do s' <- memo s
-                                                                     b' <- memo b
-                                                                     t' <- scFieldValue sc s' a b'
-                                                                     foldM reapply t' xs
     go xs                     (asPairType -> Just (a, b))       = do a' <- memo a
                                                                      b' <- memo b
                                                                      t' <- scPairType sc a' b'
                                                                      foldM reapply t' xs
-    go xs                     (asFieldType -> Just (s, a, b))   = do s' <- memo s
-                                                                     a' <- memo a
-                                                                     b' <- memo b
-                                                                     t' <- scFieldType sc s' a' b'
-                                                                     foldM reapply t' xs
     go xs                     (asRecordType -> Just elems)   = do elems' <-
                                                                     mapM (\(i,t) -> (i,) <$> memo t) (Map.assocs elems)
                                                                   t' <- scRecordType sc elems'
@@ -677,7 +653,6 @@ scWhnf sc t0 =
     reapply t (ElimApp x) = scApply sc t x
     reapply t (ElimProj i) = scRecordSelect sc t i
     reapply t (ElimPair i) = scPairSelector sc t i
-    reapply t (ElimOldProj i) = scOldRecordSelect sc t i
     reapply t (ElimRecursor d ps p_ret cs_fs ixs) =
       scFlatTermF sc (RecursorApp d ps p_ret cs_fs ixs t)
 
@@ -831,22 +806,6 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty
         PairRight t -> do
           STApp{ stAppTermF = FTermF (PairType _ t2) } <- memo t >>= liftIO . scWhnf sc
           return t2
-        EmptyValue -> lift $ scEmptyType sc
-        EmptyType -> lift $ scSort sc (mkSort 0)
-        FieldValue f x y -> do
-          tx <- memo x
-          ty <- memo y
-          lift $ scFieldType sc f tx ty
-        FieldType _ x y -> do
-          sx <- sort x
-          sy <- sort y
-          lift $ scSort sc (max sx sy)
-        RecordSelector t f -> do
-          f' <- asStringLit =<< liftIO (scWhnf sc f)
-          t' <- memo t >>= liftIO . scWhnf sc
-          m <- asRecordType t'
-          let Just tp = Map.lookup f' m
-          return tp
         CtorApp c params args -> do
           t <- lift $ scTypeOfCtor sc c
           lift $ foldM (reducePi sc) t (params ++ args)
@@ -1089,31 +1048,12 @@ scVector sc e xs = scFlatTermF sc (ArrayValue e (V.fromList xs))
 scRecord :: SharedContext -> Map FieldName Term -> IO Term
 scRecord sc m = scFlatTermF sc (RecordValue $ Map.assocs m)
 
-scOldRecord :: SharedContext -> Map FieldName Term -> IO Term
-scOldRecord sc m = go (Map.assocs m)
-  where go [] = scEmptyValue sc
-        go ((f, x) : xs) = do l <- scString sc f
-                              r <- go xs
-                              scFieldValue sc l x r
-
 scRecordSelect :: SharedContext -> Term -> FieldName -> IO Term
 scRecordSelect sc t fname = scFlatTermF sc (RecordProj t fname)
 
-scOldRecordSelect :: SharedContext -> Term -> FieldName -> IO Term
-scOldRecordSelect sc t fname = do
-  l <- scString sc fname
-  scFlatTermF sc (RecordSelector t l)
-
 scRecordType :: SharedContext -> [(String,Term)] -> IO Term
 scRecordType sc elem_tps = scFlatTermF sc (RecordType elem_tps)
 
-scOldRecordType :: SharedContext -> Map FieldName Term -> IO Term
-scOldRecordType sc m = go (Map.assocs m)
-  where go [] = scEmptyType sc
-        go ((f, x) : xs) = do l <- scString sc f
-                              r <- go xs
-                              scFieldType sc l x r
-
 scUnitValue :: SharedContext -> IO Term
 scUnitValue sc = scFlatTermF sc UnitValue
 
@@ -1126,18 +1066,6 @@ scPairValue sc x y = scFlatTermF sc (PairValue x y)
 scPairType :: SharedContext -> Term -> Term -> IO Term
 scPairType sc x y = scFlatTermF sc (PairType x y)
 
-scEmptyValue :: SharedContext -> IO Term
-scEmptyValue sc = scFlatTermF sc EmptyValue
-
-scEmptyType :: SharedContext -> IO Term
-scEmptyType sc = scFlatTermF sc EmptyType
-
-scFieldValue :: SharedContext -> Term -> Term -> Term -> IO Term
-scFieldValue sc f x y = scFlatTermF sc (FieldValue f x y)
-
-scFieldType :: SharedContext -> Term -> Term -> Term -> IO Term
-scFieldType sc f x y = scFlatTermF sc (FieldType f x y)
-
 scTuple :: SharedContext -> [Term] -> IO Term
 scTuple sc [] = scUnitValue sc
 scTuple sc (t : ts) = scPairValue sc t =<< scTuple sc ts
diff --git a/src/Verifier/SAW/Simulator.hs b/src/Verifier/SAW/Simulator.hs
index 9eaf2d28..c3af2858 100644
--- a/src/Verifier/SAW/Simulator.hs
+++ b/src/Verifier/SAW/Simulator.hs
@@ -144,19 +144,6 @@ evalTermF cfg lam recEval tf env =
                                   return $ VPairType vx vy
         PairLeft x          -> valPairLeft =<< recEval x
         PairRight x         -> valPairRight =<< recEval x
-        EmptyValue          -> return VEmpty
-        EmptyType           -> return VEmptyType
-        FieldValue f x y    -> do VString s <- recEval f
-                                  tx <- recEvalDelay x
-                                  vy <- recEval y
-                                  return $ VField s tx vy
-        FieldType f x y     -> do VString s <- recEval f
-                                  vx <- recEval x
-                                  vy <- recEval y
-                                  return $ VFieldType s vx vy
-        RecordSelector t k  -> do vt <- recEval t
-                                  VString s <- recEval k
-                                  valRecordSelect s vt
         CtorApp ident ps ts -> do v <- simGlobal cfg ident
                                   ps' <- mapM recEvalDelay ps
                                   ts' <- mapM recEvalDelay ts
diff --git a/src/Verifier/SAW/Simulator/Prims.hs b/src/Verifier/SAW/Simulator/Prims.hs
index 69e4845e..432e6a95 100644
--- a/src/Verifier/SAW/Simulator/Prims.hs
+++ b/src/Verifier/SAW/Simulator/Prims.hs
@@ -506,11 +506,6 @@ eqOp bp =
       do b1 <- go' x1 y1
          b2 <- go' x2 y2
          bpAnd bp b1 b2
-    go VEmpty VEmpty = return (bpTrue bp)
-    go (VField xf x1 x2) (VField yf y1 y2) | xf == yf =
-      do b1 <- go' x1 y1
-         b2 <- go x2 y2
-         bpAnd bp b1 b2
     go (VWord w1) (VWord w2) = bpBvEq bp w1 w2
     go (VVector v1) (VVector v2) =
       do bs <- sequence $ zipWith go' (V.toList v1) (V.toList v2)
@@ -1094,9 +1089,6 @@ muxValue bp b = value
                                                   value x y
     value VUnit             VUnit             = return VUnit
     value (VPair x1 x2)     (VPair y1 y2)     = VPair <$> thunk x1 y1 <*> thunk x2 y2
-    value VEmpty            VEmpty            = return VEmpty
-    value (VField xf x1 x2) (VField yf y1 y2) | xf == yf
-                                              = VField xf <$> thunk x1 y1 <*> value x2 y2
     value (VRecordValue elems1) (VRecordValue
                                  (alistAllFields (map fst elems1) ->
                                   Just elems2)) =
diff --git a/src/Verifier/SAW/Simulator/Value.hs b/src/Verifier/SAW/Simulator/Value.hs
index 851ecc55..d0104d45 100644
--- a/src/Verifier/SAW/Simulator/Value.hs
+++ b/src/Verifier/SAW/Simulator/Value.hs
@@ -46,8 +46,6 @@ data Value l
   = VFun !(Thunk l -> MValue l)
   | VUnit
   | VPair (Thunk l) (Thunk l) -- TODO: should second component be strict?
-  | VEmpty
-  | VField FieldName (Thunk l) !(Value l)
   | VCtorApp !Ident !(Vector (Thunk l))
   | VVector !(Vector (Thunk l))
   | VVecType (Value l) (Value l)
@@ -64,8 +62,6 @@ data Value l
   | VPiType !(Value l) !(Thunk l -> MValue l)
   | VUnitType
   | VPairType (Value l) (Value l)
-  | VEmptyType
-  | VFieldType FieldName !(Value l) !(Value l)
   | VDataType !Ident [Value l]
   | VRecordType ![(String, Value l)]
   | VRecordValue ![(String, Thunk l)]
@@ -131,8 +127,6 @@ instance Show (Extra l) => Show (Value l) where
       VFun {}        -> showString "<<fun>>"
       VUnit          -> showString "()"
       VPair{}        -> showString "<<tuple>>"
-      VEmpty         -> showString "{}"
-      VField f _ _   -> showString "{" . showString f . showString " = _, ...}"
       VCtorApp s xv
         | V.null xv  -> shows s
         | otherwise  -> shows s . showList (toList xv)
@@ -151,8 +145,6 @@ instance Show (Extra l) => Show (Value l) where
                         (shows t . showString " -> ...")
       VUnitType      -> showString "#()"
       VPairType x y  -> showParen True (shows x . showString " * " . shows y)
-      VEmptyType {}  -> showString "<<record type>>"
-      VFieldType {}  -> showString "<<record type>>"
       VDataType s vs
         | null vs    -> shows s
         | otherwise  -> shows s . showList vs
@@ -208,12 +200,6 @@ asVTupleType :: Value l -> Maybe [Value l]
 asVTupleType (VRecordType elems) = recordAListAsTuple elems
 asVTupleType _ = Nothing
 
-valRecordSelect :: (VMonad l, Show (Extra l)) =>
-  FieldName -> Value l -> MValue l
-valRecordSelect k (VField k' x r) = if k == k' then force x else valRecordSelect k r
-valRecordSelect k VEmpty = fail $ "valRecordSelect: record field not found: " ++ k
-valRecordSelect _ v = fail $ "valRecordSelect: Not a record value: " ++ show v
-
 valRecordProj :: (VMonad l, Show (Extra l)) => Value l -> String -> MValue l
 valRecordProj (VRecordValue fld_map) fld
   | Just t <- lookup fld fld_map = force t
@@ -244,13 +230,6 @@ asFiniteTypeValue v =
       case t2 of
         FTTuple ts -> return (FTTuple (t1 : ts))
         _ -> Nothing
-    VEmptyType -> return (FTRec Map.empty)
-    VFieldType k v1 v2 -> do
-      t1 <- asFiniteTypeValue v1
-      t2 <- asFiniteTypeValue v2
-      case t2 of
-        FTRec tm -> return (FTRec (Map.insert k t1 tm))
-        _ -> Nothing
     VRecordType elem_tps ->
       FTRec <$> Map.fromList <$>
       mapM (\(fld,tp) -> (fld,) <$> asFiniteTypeValue tp) elem_tps
diff --git a/src/Verifier/SAW/Term/Functor.hs b/src/Verifier/SAW/Term/Functor.hs
index b9616d82..e5a7b45c 100644
--- a/src/Verifier/SAW/Term/Functor.hs
+++ b/src/Verifier/SAW/Term/Functor.hs
@@ -257,11 +257,6 @@ data FlatTermF e
   | PairType e e
   | PairLeft e
   | PairRight e
-  | EmptyValue
-  | EmptyType
-  | FieldValue e e e -- Field name, field value, remainder of record
-  | FieldType e e e
-  | RecordSelector e e -- Record value, field name
 
     -- | An inductively-defined type, applied to parameters and type indices
   | DataTypeApp !Ident ![e] ![e]
@@ -353,15 +348,6 @@ zipWithFlatTermF f = go
     go (PairLeft x) (PairLeft y) = Just (PairLeft (f x y))
     go (PairRight x) (PairRight y) = Just (PairLeft (f x y))
 
-    go EmptyValue EmptyValue = Just EmptyValue
-    go EmptyType EmptyType = Just EmptyType
-    go (FieldValue x1 x2 x3) (FieldValue y1 y2 y3) =
-      Just $ FieldValue (f x1 y1) (f x2 y2) (f x3 y3)
-    go (FieldType x1 x2 x3) (FieldType y1 y2 y3) =
-      Just $ FieldType (f x1 y1) (f x2 y2) (f x3 y3)
-    go (RecordSelector x1 x2) (RecordSelector y1 y2) =
-      Just $ RecordSelector (f x1 y1) (f x2 y2)
-
     go (CtorApp cx psx lx) (CtorApp cy psy ly)
       | cx == cy = Just $ CtorApp cx (zipWith f psx psy) (zipWith f lx ly)
     go (DataTypeApp dx psx lx) (DataTypeApp dy psy ly)
diff --git a/src/Verifier/SAW/Term/Pretty.hs b/src/Verifier/SAW/Term/Pretty.hs
index 81bace26..e1bbd0f3 100644
--- a/src/Verifier/SAW/Term/Pretty.hs
+++ b/src/Verifier/SAW/Term/Pretty.hs
@@ -334,20 +334,6 @@ ppRecord type_p alist =
 ppProj :: String -> Doc -> Doc
 ppProj sel doc = doc <> char '.' <> text sel
 
--- | Pretty-print an old-style record field value
-ppOldFieldValue :: Doc -> Doc -> Doc -> Doc
-ppOldFieldValue f x y =
-  braces (eqn f x <+> char '|' <+> y)
-  where eqn l r = group (nest 2 (l <+> equals <<$>> r))
-
--- | Pretty-print an old-style record field type
-ppOldFieldType :: Doc -> Doc -> Doc -> Doc
-ppOldFieldType f x y = char '#' <> ppOldFieldValue f x y
-
--- | Pretty-print an old-style record selector @x.(f)@
-ppOldRecordSel :: Doc -> Doc -> Doc
-ppOldRecordSel x f = x <> char '.' <> parens f
-
 -- | Pretty-print an array value @[v1, ..., vn]@
 ppArrayValue :: [Doc] -> Doc
 ppArrayValue = list
@@ -398,22 +384,13 @@ ppFlatTermF :: Prec -> FlatTermF Term -> PPM Doc
 ppFlatTermF prec tf =
   case tf of
     GlobalDef i   -> return $ ppIdent i
-    UnitValue     -> return $ text "()"
-    UnitType      -> return $ text "#()"
+    UnitValue     -> return $ text "(-empty-)"
+    UnitType      -> return $ text "#(-empty-)"
     PairValue x y -> ppPair <$> ppTerm' PrecNone x <*> ppTerm' PrecNone y
     PairType x y  -> ppPairType <$> ppTerm' PrecNone x <*> ppTerm' PrecNone y
     PairLeft t    -> ppProj "1" <$> ppTerm' PrecArg t
     PairRight t   -> ppProj "2" <$> ppTerm' PrecArg t
-    EmptyValue          -> return $ text "{}"
-    EmptyType           -> return $ text "#{}"
-    FieldValue f x y    ->
-      ppOldFieldValue <$> ppTerm' PrecNone f <*>
-      ppTerm' PrecNone x <*> ppTerm' PrecNone y
-    FieldType f x y     ->
-      ppOldFieldType <$> ppTerm' PrecNone f <*>
-      ppTerm' PrecNone x <*> ppTerm' PrecNone y
-    RecordSelector t f  ->
-      ppOldRecordSel <$> ppTerm' PrecArg t <*> ppTerm' PrecArg f
+
     CtorApp c params args ->
       ppAppList prec (ppIdent c) <$> mapM (ppTerm' PrecArg) (params ++ args)
     DataTypeApp dt params args ->
@@ -517,8 +494,6 @@ shouldMemoizeTerm t =
     FTermF GlobalDef{} -> False
     FTermF UnitValue -> False
     FTermF UnitType -> False
-    FTermF EmptyValue -> False
-    FTermF EmptyType -> False
     FTermF (CtorApp _ [] []) -> False
     FTermF (DataTypeApp _ [] []) -> False
     FTermF Sort{} -> False