diff -r 56617a7b68c5 -r 97e9dae57284 src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Tue Jun 10 16:43:07 2008 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy	Tue Jun 10 16:43:14 2008 +0200
@@ -54,7 +54,7 @@
   \<Longrightarrow> (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) = 
      the (loc x)"
 apply (simp only: index_def gjmb_plns_def)
-apply (case_tac "(gmb G C S)")
+apply (case_tac "gmb G C S" rule: prod.exhaust)
 apply (simp add: galldefs del: set_append map_append)
 apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
 apply (intro strip)
@@ -74,7 +74,7 @@
   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)", simp)
+apply (case_tac "gmb G C S" rule: prod.exhaust, simp)
 apply (case_tac b, simp)
 apply (rule conjI)
 apply (simp add: gl_def)