--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Sep 09 20:51:36 2014 +0200
@@ -95,15 +95,15 @@
apply simp
apply (case_tac a)
apply auto
- apply (case_tac prim_ty)
+ apply (rename_tac prim_ty, case_tac prim_ty)
apply auto
- apply (case_tac prim_ty)
+ apply (rename_tac prim_ty, case_tac prim_ty)
apply auto
apply (case_tac list)
apply auto
apply (case_tac a)
apply auto
- apply (case_tac prim_ty)
+ apply (rename_tac prim_ty, case_tac prim_ty)
apply auto
done