changeset 58263 | 6c907aad90ba |
parent 55466 | 786edc984c98 |
child 58886 | 8a6cac7c7247 |
--- a/src/HOL/MicroJava/J/Conform.thy Tue Sep 09 20:51:36 2014 +0200 +++ b/src/HOL/MicroJava/J/Conform.thy Tue Sep 09 20:51:36 2014 +0200 @@ -108,7 +108,7 @@ apply (unfold conf_def) apply (rule_tac y = "T" in ty.exhaust) apply (erule ssubst) -apply (rule_tac y = "prim_ty" in prim_ty.exhaust) +apply (rename_tac prim_ty, rule_tac y = "prim_ty" in prim_ty.exhaust) apply (auto simp add: widen.null) done