diff -r 62a0d10386c1 -r e65ab21821bf src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/MicroJava/Comp/Index.thy	Sun Sep 30 18:19:28 2018 -0400
@@ -70,7 +70,7 @@
 lemma update_at_index: "
   \<lbrakk> distinct (gjmb_plns (gmb G C S));
   x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>
-  locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
+  (locvars_xstate G C S (Norm (h, l)))[index (gmb G C S) x := val] =
   locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
   apply (simp only: locvars_xstate_def locvars_locals_def index_def)
   apply (case_tac "gmb G C S" rule: prod.exhaust, simp)