diff --git a/spec/design/skel/FaultHandler_H.thy b/spec/design/skel/FaultHandler_H.thy
index f50b665453..702a23e1a2 100644
--- a/spec/design/skel/FaultHandler_H.thy
+++ b/spec/design/skel/FaultHandler_H.thy
@@ -17,7 +17,7 @@ arch_requalify_consts (H)
   makeArchFaultMessage
   handleArchFaultReply
 
-(* FIXME arch-split: clobbers generic with arch version, no disambiguation via global. *)
+(* clobbers previously requalified abstract spec constants with design spec versions *)
 arch_requalify_consts (aliasing, H)
   syscallMessage
   exceptionMessage
diff --git a/spec/design/skel/Invocations_H.thy b/spec/design/skel/Invocations_H.thy
index c7b8fd9653..8ef06a4248 100644
--- a/spec/design/skel/Invocations_H.thy
+++ b/spec/design/skel/Invocations_H.thy
@@ -19,7 +19,7 @@ requalify_types (in Arch)
 #INCLUDE_HASKELL SEL4/API/Invocation.lhs Arch=Arch NOT GenInvocationLabels InvocationLabel
 #INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs ONLY invocationType genInvocationType
 
-(* disambiguate Arch.invocation vs global.invocation *)
+(* disambiguate name clash between Arch and non-arch consts with same names *)
 context Arch begin
 context begin global_naming global
 requalify_types (aliasing)
diff --git a/spec/design/skel/KernelInit_H.thy b/spec/design/skel/KernelInit_H.thy
index c930f13556..9ea945b143 100644
--- a/spec/design/skel/KernelInit_H.thy
+++ b/spec/design/skel/KernelInit_H.thy
@@ -73,7 +73,7 @@ newKernelState_def:
         ksMachineState = init_machine_state
 \<rparr>"
 
-(* disambiguate newKernelState defined here as global vs the one in Arch as Arch *)
+(* disambiguate name clash between Arch and non-arch consts with same names *)
 context Arch begin
 requalify_facts (aliasing)
    newKernelState_def
diff --git a/spec/design/skel/TCBDecls_H.thy b/spec/design/skel/TCBDecls_H.thy
index 6b5829dc13..9cd752d572 100644
--- a/spec/design/skel/TCBDecls_H.thy
+++ b/spec/design/skel/TCBDecls_H.thy
@@ -10,6 +10,7 @@ theory TCBDecls_H
 imports FaultMonad_H Invocations_H
 begin
 
-#INCLUDE_HASKELL SEL4/Object/TCB.lhs decls_only NOT archThreadGet archThreadSet
+#INCLUDE_HASKELL SEL4/Object/TCB.lhs decls_only \
+  NOT archThreadGet archThreadSet sanitiseRegister getSanitiseRegisterInfo
 
 end
diff --git a/spec/design/skel/TCB_H.thy b/spec/design/skel/TCB_H.thy
index 4d11654390..5c9b070e1c 100644
--- a/spec/design/skel/TCB_H.thy
+++ b/spec/design/skel/TCB_H.thy
@@ -22,15 +22,14 @@ arch_requalify_consts (H)
   msgRegisters
   fromVPtr
   postModifyRegisters
+  sanitiseRegister
+  getSanitiseRegisterInfo
 
-(* FIXME arch-split: not clear why this is being done this way, there's no disambiguation *)
-(* override generic names with arch-specific versions *)
+(* clobbers previously requalified abstract spec constants with design spec versions *)
 arch_requalify_consts (aliasing, H)
   gpRegisters
   frameRegisters
   tlsBaseRegister
-  sanitiseRegister
-  getSanitiseRegisterInfo
 
 abbreviation "mapMaybe \<equiv> option_map"