src/HOL/Nominal/Examples/Fsub.thy

--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Feb 12 08:37:06 2014 +0100
@@ -167,7 +167,8 @@
   assumes a: "X\<in>(ty_dom \<Gamma>)" 
   shows "\<exists>T.(TVarB X T)\<in>set \<Gamma>"
   using a 
-  apply (induct \<Gamma>, auto) 
+  apply (induct \<Gamma>, auto)
+  apply (rename_tac a \<Gamma>') 
   apply (subgoal_tac "\<exists>T.(TVarB X T=a)")
   apply (auto)
   apply (auto simp add: ty_binding_existence)