DatatypePackage.case_tac;

--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Jun 09 17:07:11 2008 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Jun 09 17:24:48 2008 +0200
@@ -247,7 +247,7 @@
        THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
 
 -- "for if"
-apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW
+apply( tactic {* (DatatypePackage.case_tac "the_Bool v" THEN_ALL_NEW
   (asm_full_simp_tac @{simpset})) 7*})
 
 apply (tactic "forward_hyp_tac")