diff --git a/spec/abstract/X64/FPU_A.thy b/spec/abstract/X64/FPU_A.thy
index 0890c68f8a..576714a714 100644
--- a/spec/abstract/X64/FPU_A.thy
+++ b/spec/abstract/X64/FPU_A.thy
@@ -25,7 +25,7 @@ definition load_fpu_state :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad
      do_machine_op (writeFpuState fpu_state)
    od"
 
-\<comment> \<open>FIXME: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\<close>
+\<comment> \<open>FIXME FPU: maybe use an if instead of the case (depends on if wpc or if\_split is easier)\<close>
 definition switch_local_fpu_owner :: "obj_ref option \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "switch_local_fpu_owner new_owner \<equiv> do
      do_machine_op enableFpu;