src/HOL/Proofs/Lambda/WeakNorm.thy

   assume "NF t"
   thus "\<And>e T' u i. PROP ?Q t e T' u i T"
   proof induct
     fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
     {
-      case (App ts x e_ T'_ u_ i_)
+      case (App ts x e1 T'1 u1 i1)
       assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
       then obtain Us
         where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
         and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"
         by (rule var_app_typesE)

           assume "\<not> (i < x)"
           with NF neq show ?thesis by (simp add: subst_Var) iprover
         qed
       qed
     next
-      case (Abs r e_ T'_ u_ i_)
+      case (Abs r e1 T'1 u1 i1)
       assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
       then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
       moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
       moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
       ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)