diff -r a29006291f2b -r 125e49d04cf6 src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:42:05 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:48:28 2012 +0100
@@ -127,7 +127,7 @@
 lemma wf_java_mdecl_disjoint_varnames: 
   "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) 
   \<Longrightarrow> disjoint_varnames pns lvars"
-apply (case_tac S)
+apply (cases S)
 apply (simp add: wf_java_mdecl_def disjoint_varnames_def  map_of_in_set)
 done