# HG changeset patch
# User wenzelm
# Date 1213108996 -7200
# Node ID 9a26c0d7a47a84d3a4d018629d154ff74b497de2
# Parent  97e9dae572841123bde5f05add4706429190cc92
tuned proofs;

diff -r 97e9dae57284 -r 9a26c0d7a47a src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Jun 10 16:43:14 2008 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Jun 10 16:43:16 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 {* (DatatypePackage.case_tac "the_Bool v" THEN_ALL_NEW
+apply( tactic {* (case_split_tac "the_Bool v" THEN_ALL_NEW
   (asm_full_simp_tac @{simpset})) 7*})
 
 apply (tactic "forward_hyp_tac")