1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 28 13:19:25 2013 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 28 13:24:51 2013 +0100
     1.3 @@ -198,7 +198,7 @@
     1.4  
     1.5  -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
     1.6  apply( simp_all)
     1.7 -apply( tactic "ALLGOALS strip_tac")
     1.8 +apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
     1.9  apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
    1.10                   THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
    1.11  apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")