diff --git a/proof/refine/RISCV64/Invariants_H.thy b/proof/refine/RISCV64/Invariants_H.thy
index 487c4de92..5de6eed78 100644
--- a/proof/refine/RISCV64/Invariants_H.thy
+++ b/proof/refine/RISCV64/Invariants_H.thy
@@ -641,7 +641,7 @@ definition
   (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)"
 
 definition
-  parentOf :: "cte_heap \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> bool" ("_ \<turnstile> _ parentOf _")
+  parentOf :: "cte_heap \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> bool" ("_ \<turnstile> _ parentOf _" [60,0,60] 61)
 where
   "s \<turnstile> c' parentOf c \<equiv>
   \<exists>cte' cte. s c = Some cte \<and> s c' = Some cte' \<and> isMDBParentOf cte' cte"