diff --git a/reactos/ntoskrnl/include/internal/ke.h b/reactos/ntoskrnl/include/internal/ke.h
index 34e1ae0cbc2..f2a4a2f705e 100644
--- a/reactos/ntoskrnl/include/internal/ke.h
+++ b/reactos/ntoskrnl/include/internal/ke.h
@@ -151,6 +151,70 @@ extern ULONG KiDPCTimeout;
 /* One of the Reserved Wait Blocks, this one is for the Thread's Timer */
 #define TIMER_WAIT_BLOCK 0x3L
 
+#ifdef _M_ARM // FIXME: remove this once our headers are cleaned up
+// 
+// A system call ID is formatted as such:
+// .________________________________________________________________.
+// | 14 | 13 | 12 | 11 | 10 | 9 | 8 | 7 | 6 | 5 | 4 | 3 | 2 | 1 | 0 |
+// |--------------|-------------------------------------------------|
+// | TABLE NUMBER |                  TABLE OFFSET                   |
+// \----------------------------------------------------------------/
+//
+//
+// The table number is then used as an index into the service descriptor table.
+#define TABLE_NUMBER_BITS 3
+#define TABLE_OFFSET_BITS 12
+
+//
+// There are 2 tables (kernel and shadow, used by Win32K)
+//
+#define NUMBER_SERVICE_TABLES 2
+#define NTOS_SERVICE_INDEX   0
+#define WIN32K_SERVICE_INDEX 1
+
+//
+// NB. From assembly code, the table number must be computed as an offset into
+//     the service descriptor table.
+//     
+//     Each entry into the table is 16 bytes long on 32-bit architectures, and
+//     32 bytes long on 64-bit architectures.
+//
+//     Thus, Table Number 1 is offset 16 (0x10) on x86, and offset 32 (0x20) on
+//     x64.
+//
+#ifdef _WIN64
+#define BITS_PER_ENTRY 5 // (1 << 5) = 32 bytes
+#else
+#define BITS_PER_ENTRY 4 // (1 << 4) = 16 bytes
+#endif
+
+//
+// We want the table number, but leave some extra bits to we can have the offset
+// into the descriptor table.
+//
+#define SERVICE_TABLE_SHIFT (12 - BITS_PER_ENTRY)
+
+//
+// Now the table number (as an offset) is corrupted with part of the table offset
+// This mask will remove the extra unwanted bits, and give us the offset into the
+// descriptor table proper.
+//
+#define SERVICE_TABLE_MASK  (((1 << TABLE_NUMBER_BITS) - 1) << BITS_PER_ENTRY)
+
+//
+// To get the table offset (ie: the service call number), just keep the 12 bits
+//
+#define SERVICE_NUMBER_MASK ((1 << TABLE_OFFSET_BITS) - 1)
+
+//
+// We'll often need to check if this is a graphics call. This is done by comparing
+// the table number offset with the known Win32K table number offset.
+// This is usually index 1, so table number offset 0x10 (x86) or 0x20 (x64)
+//
+#define SERVICE_TABLE_TEST  (WIN32K_SERVICE_INDEX << BITS_PER_ENTRY)
+
+#endif
+
 /* INTERNAL KERNEL FUNCTIONS ************************************************/
 
 VOID