src/HOL/Bali/Evaln.thy
changeset 58251 b13e5c3497f5
parent 56199 8e8d28ed7529
child 58887 38db8ddc0f57
--- a/src/HOL/Bali/Evaln.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Bali/Evaln.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -245,7 +245,7 @@
   | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
 apply (erule evaln_cases , auto)
 apply (induct_tac "t")
-apply   (induct_tac "a")
+apply   (rename_tac a, induct_tac "a")
 apply auto
 done