diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Fri Sep 27 16:44:50 2002 +0200
+++ b/src/HOL/Lambda/Type.thy	Mon Sep 30 15:44:21 2002 +0200
@@ -332,7 +332,7 @@
     assume uIT: "u \<in> IT"
     assume uT: "e \<turnstile> u : T"
     {
-      case (Var n rs)
+      case (Var n rs e_ T'_ u_ i_)
       assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
       let ?ty = "{t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'}"
       let ?R = "\<lambda>t. \<forall>e T' u i.
@@ -440,13 +440,13 @@
         with False show ?thesis by (auto simp add: subst_Var)
       qed
     next
-      case (Lambda r)
+      case (Lambda r e_ T'_ u_ i_)
       assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
         and "\<And>e T' u i. PROP ?Q r e T' u i T"
       with uIT uT show "Abs r[u/i] \<in> IT"
         by fastsimp
     next
-      case (Beta r a as)
+      case (Beta r a as e_ T'_ u_ i_)
       assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
       assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
       assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"