| changeset 58263 | 6c907aad90ba |
| parent 42463 | f270e3e18be5 |
| child 58886 | 8a6cac7c7247 |
--- a/src/HOL/MicroJava/J/WellType.thy Tue Sep 09 20:51:36 2014 +0200 +++ b/src/HOL/MicroJava/J/WellType.thy Tue Sep 09 20:51:36 2014 +0200 @@ -94,7 +94,7 @@ lemma typeof_default_val: "\<exists>T. (typeof dt (default_val ty) = Some T) \<and> G\<turnstile> T \<preceq> ty" apply (case_tac ty) -apply (case_tac prim_ty) +apply (rename_tac prim_ty, case_tac prim_ty) apply auto done