--- a/src/HOL/MicroJava/Comp/Index.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy Wed Feb 12 08:37:06 2014 +0100
@@ -54,6 +54,7 @@
apply (simp only: index_def gjmb_plns_def)
apply (case_tac "gmb G C S" rule: prod.exhaust)
apply (simp add: galldefs del: set_append map_append)
+apply (rename_tac a b)
apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
apply (intro strip)
apply (simp del: set_append map_append)
@@ -73,6 +74,7 @@
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)
+apply (rename_tac a b)
apply (case_tac b, simp)
apply (rule conjI)
apply (simp add: gl_def)