diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Mar 13 07:07:07 2014 +0100
@@ -1268,7 +1268,6 @@
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (rule exI)+
   apply (simp add: wf_prog_ws_prog [THEN comp_method])
-  apply auto
   done
 
 
@@ -2517,16 +2516,13 @@
                               (start_ST, start_LT C pTs (length lvars))))
                 = (start_ST, inited_LT C pTs lvars)") 
    prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption
-apply (simp only:)
 apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
                        (start_ST, inited_LT C pTs lvars))) 
                 = (start_ST, inited_LT C pTs lvars)") 
    prefer 2 apply (erule conjE)+
    apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+
    apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
-apply (simp only:)
-apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
-   apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
+   apply (simp (no_asm_simp) add: is_inited_LT_def)
 
 
    (* Return *)