diff -r ace45a11a45e -r bad75618fb82 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -981,7 +981,8 @@
     from fvar obtain upd w
       where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and
               v: "v=(w,upd)"
-      by (cases "fvar statDeclC stat fn a s2") simp
+      by (cases "fvar statDeclC stat fn a s2")
+        (simp, use surjective_pairing in blast)
     {
       fix j val fix s::state
       assume "normal s3"
@@ -1025,7 +1026,8 @@
     from avar obtain upd w
       where upd: "upd = snd (fst (avar G i a s2))" and
               v: "v=(w,upd)"
-      by (cases "avar G i a s2") simp
+      by (cases "avar G i a s2")
+        (simp, use surjective_pairing in blast)
     {
       fix j val fix s::state
       assume "normal s2'"