src/HOL/MicroJava/J/JTypeSafe.thy

--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 12 22:21:38 2011 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 12 22:48:23 2011 +0200
@@ -243,7 +243,7 @@
        THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
 
 -- "for if"
-apply( tactic {* (InductTacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
+apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
   (asm_full_simp_tac @{simpset})) 7*})
 
 apply (tactic "forward_hyp_tac")