[squash] design: clear up requalify clobbering situation

* Do not import generic constants sanitiseRegister and getSanitiseRegisterInfo.
  Their definitions were never imported in lieu of using translated Arch
  versions that have the same type, causing aliasing warning during
  const requalification.
* Update comments where requalify clobbers arch version from abstract
  spec.

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

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)

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

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

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"