capdDL-api: update to Isabelle2023 mapsto syntax

Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Oct 6, 2023 · 4c0b3df · 4c0b3df
1 parent f7768ee
commit 4c0b3df
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/proof/capDL-api/Invocation_DP.thy b/proof/capDL-api/Invocation_DP.thy
@@ -1142,13 +1142,13 @@ lemma sep_map_c_asid_reset:
    apply clarsimp
    apply (case_tac "\<not> has_slots obj")
     apply simp
-   apply (rule_tac x = "update_slots (object_slots obj(snd ptr \<mapsto> cap')) obj"
+   apply (rule_tac x = "update_slots ((object_slots obj)(snd ptr \<mapsto> cap')) obj"
      in exI)
    apply (simp add:sep_map_general_def object_to_sep_state_slot)
   apply clarsimp
   apply (case_tac "\<not> has_slots obj")
    apply simp
-  apply (rule_tac x = "update_slots (object_slots obj(snd ptr \<mapsto> cap)) obj"
+  apply (rule_tac x = "update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj"
     in exI)
   apply (simp add:sep_map_general_def object_to_sep_state_slot)
   done