src/ZF/Coind/Types.thy

--- a/src/ZF/Coind/Types.thy	Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/Coind/Types.thy	Wed Jul 10 16:54:07 2002 +0200
@@ -54,8 +54,7 @@
 lemma te_appI:
      "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty"
 apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp)
-apply (erule TyEnv.induct)
-apply auto
+apply (erule TyEnv.induct, auto)
 done