src/HOL/MicroJava/Comp/CorrComp.thy

 apply (frule wtpd_expr_binop)
 (* establish (s1::\<preceq> \<dots>) *)
 apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) 
 
 
-apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
 apply (case_tac bop)
   (*subcase bop = Eq *)  apply simp apply (rule progression_Eq)
   (*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp

 apply (intro allI impI)
    (* establish x1 = None \<and> a' \<noteq> Null *)
 apply (simp (no_asm_use) only: gx_conv, frule np_NoneD)
 apply (frule wtpd_expr_facc)
 
-apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
 apply blast
 apply (rule progression_one_step)
 apply (simp add: gh_def)
 apply (case_tac "(the (fst s1 (the_Addr a')))")

 
   (* establish ((Norm s1)::\<preceq> \<dots>) *)
 apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) 
    apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) 
 
-apply (simp only: compExpr_compExprs.simps)
+apply (simp only: compExpr.simps compExprs.simps)
 
 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
 apply fast (* blast does not seem to work - why? *)
 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
 apply fast

 apply (frule method_preserves_length, assumption, assumption) 
 (* establish length pvs = length ps *)
 apply (frule evals_preserves_length [THEN sym])
 
 (** start evaluating subexpressions **)
-apply (simp (no_asm_use) only: compExpr_compExprs.simps)
+apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
 
   (* evaluate e *)
 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
 apply fast