diff --git a/spec/cspec/RISCV64/Kernel_C.thy b/spec/cspec/RISCV64/Kernel_C.thy
index e00f5e2269..893fe1789c 100644
--- a/spec/cspec/RISCV64/Kernel_C.thy
+++ b/spec/cspec/RISCV64/Kernel_C.thy
@@ -29,11 +29,16 @@ type_synonym cghost_state =
   "(machine_word \<rightharpoonup> vmpage_size) * (machine_word \<rightharpoonup> nat) * ghost_assertions *
    (machine_word \<rightharpoonup> nat)"
 
+abbreviation gs_refill_buffer_lengths :: "cghost_state \<Rightarrow> (machine_word \<rightharpoonup> nat)" where
+  "gs_refill_buffer_lengths \<equiv> snd \<circ> snd \<circ> snd"
+
 definition
   gs_clear_region :: "addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state" where
   "gs_clear_region ptr bits gs \<equiv>
-   (%x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
-    %x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x, snd (snd gs))"
+   (\<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst gs x,
+    \<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else fst (snd gs) x,
+    fst (snd (snd gs)),
+    \<lambda>x. if x \<in> {ptr..+2 ^ bits} then None else gs_refill_buffer_lengths gs x)"
 
 definition
   gs_new_frames:: "vmpage_size \<Rightarrow> addr \<Rightarrow> nat \<Rightarrow> cghost_state \<Rightarrow> cghost_state"
@@ -53,9 +58,6 @@ definition
                      then Some sz
                      else fst (snd gs) x, snd (snd gs))"
 
-abbreviation gs_refill_buffer_lengths :: "cghost_state \<Rightarrow> (machine_word \<rightharpoonup> nat)" where
-  "gs_refill_buffer_lengths \<equiv> snd \<circ> snd \<circ> snd"
-
 abbreviation (input) refills_len :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "refills_len userSize struct_size refill_size \<equiv> (2 ^ userSize - struct_size) div refill_size"