autocorres: update to Isabelle2023

Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Oct 6, 2023 · 0f99a75 · 0f99a75
1 parent 4c0b3df
commit 0f99a75
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/tools/autocorres/TypHeapSimple.thy b/tools/autocorres/TypHeapSimple.thy
@@ -512,7 +512,7 @@ lemma simple_lift_field_update':
   and   xf_xfu: "fg_cons xf xfu"
   and       cl: "simple_lift hp ptr = Some z"
   shows "(simple_lift (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>f)) val) hp)) =
-                simple_lift hp(ptr \<mapsto> xfu val z)"
+                (simple_lift hp)(ptr \<mapsto> xfu val z)"
     (is "?LHS = ?RHS")
 proof (rule ext)
   fix p
@@ -581,7 +581,7 @@ lemma simple_lift_field_update:
   and   xf_xfu: "fg_cons xf (xfu o (\<lambda>x _. x))"
   and       cl: "simple_lift hp ptr = Some z"
   shows "(simple_lift (hrs_mem_update (heap_update (Ptr &(ptr\<rightarrow>f)) val) hp)) =
-                simple_lift hp(ptr \<mapsto> xfu (\<lambda>_. val) z)"
+                (simple_lift hp)(ptr \<mapsto> xfu (\<lambda>_. val) z)"
     (is "?LHS = ?RHS")
   apply (insert fl [unfolded field_ti_def])
   apply (clarsimp split: option.splits)

diff --git a/tools/autocorres/utils.ML b/tools/autocorres/utils.ML
@@ -459,7 +459,7 @@ fun term_fold_map_top f x =
  *)
 fun simp_map f =
   Context.map_proof (
-    Local_Theory.declaration {syntax = false, pervasive = false} (
+    Local_Theory.declaration {syntax = false, pervasive = false, pos = @{here}} (
       K (Simplifier.map_ss f)))
   |> Context.proof_map