diff --git a/mps/code/mpm.h b/mps/code/mpm.h
index b53acf252eb..eb52f275de8 100644
--- a/mps/code/mpm.h
+++ b/mps/code/mpm.h
@@ -805,8 +805,6 @@ extern void BufferRampReset(Buffer buffer);
 
 extern Res BufferFramePush(AllocFrame *frameReturn, Buffer buffer);
 extern Res BufferFramePop(Buffer buffer, AllocFrame frame);
-extern FrameState BufferFrameState(Buffer buffer);
-extern void BufferFrameSetState(Buffer buffer, FrameState state);
 
 
 /* DEFINE_BUFFER_CLASS -- define a buffer class */
diff --git a/mps/code/mpmtypes.h b/mps/code/mpmtypes.h
index 6989ded5d8d..06527f00923 100644
--- a/mps/code/mpmtypes.h
+++ b/mps/code/mpmtypes.h
@@ -71,7 +71,6 @@ typedef struct BufferClassStruct *BufferClass; /* <design/buffer/> */
 typedef BufferClass SegBufClass;        /* <design/buffer/> */
 typedef BufferClass RankBufClass;       /* <design/buffer/> */
 typedef unsigned BufferMode;            /* <design/buffer/> */
-typedef unsigned FrameState;            /* <design/alloc-frame/> */
 typedef struct mps_fmt_s *Format;       /* design.mps.format */
 typedef struct LockStruct *Lock;        /* <code/lock.c>* */
 typedef struct mps_pool_s *Pool;        /* <design/pool/> */
diff --git a/mps/design/type.txt b/mps/design/type.txt
index c90a9335456..a140b33fad9 100644
--- a/mps/design/type.txt
+++ b/mps/design/type.txt
@@ -277,29 +277,6 @@ Value                 Description
 ====================  ==================================================
 
 
-``typedef unsigned FrameState``
-
-_`.framestate`: ``FrameState`` represents the current state in a
-buffer frame's lifecycle. See design.mps.alloc-frame_. It takes one of
-the following values:
-
-.. _design.mps.alloc-frame: alloc-frame
-
-==========================  ============================================
-State                       Description
-==========================  ============================================
-``BufferFrameVALID``        Indicates that ``PushFrame()`` can be a
-                            lightweight operation and need not be
-                            synchronized.
-``BufferFramePOP_PENDING``  Indicates that there has been a
-                            ``PopFrame()`` operation that the pool
-                            must respond to.
-``BufferFrameDISABLED``     Indicates that the pool has disabled
-                            support for lightweight operations for
-                            this buffer.
-==========================  ============================================
-
-
 ``typedef void (*Fun)(void)``
 
 _`.fun`: ``Fun`` is the type of a pointer to a function about which
diff --git a/mps/manual/source/extensions/mps/designs.py b/mps/manual/source/extensions/mps/designs.py
index 3bf60a006b7..e54ed64e8d6 100644
--- a/mps/manual/source/extensions/mps/designs.py
+++ b/mps/manual/source/extensions/mps/designs.py
@@ -20,7 +20,7 @@ TYPES = '''
 
     AccessSet Accumulation Addr Align AllocFrame AllocPattern AP Arg
     Arena Attr Bool BootBlock BT Buffer BufferMode Byte Chain Chunk
-    Clock Compare Count Epoch FindDelete Format FrameState Fun GenDesc
+    Clock Compare Count Epoch FindDelete Format Fun GenDesc
     Globals Index Land LD Lock LocusPref LocusPrefKind Message
     MessageType MutatorFaultContext Page Pointer Pool PoolGen
     PThreadext Range Rank RankSet ReadonlyAddr Ref RefSet Res