diff -r c7c38c901267 -r 9999d7823b8f src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -130,7 +130,7 @@
   assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
   shows "cl \<in> array_ran a h \<or> cl = b"
 proof -
-  have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
+  have "set ((Array.get h a)[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
   with assms show ?thesis 
     unfolding array_ran_def Array.update_def by fastforce
 qed
@@ -139,7 +139,7 @@
   assumes "cl \<in> array_ran a (Array.update a i None h)"
   shows "cl \<in> array_ran a h"
 proof -
-  have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
+  have "set ((Array.get h a)[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
   with assms show ?thesis
     unfolding array_ran_def Array.update_def by auto
 qed