diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Lambda/Type.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -121,7 +121,7 @@
   apply (case_tac Ts)
   apply simp+
   apply (case_tac Ts)
-  apply (case_tac "list @ [t]")
+  apply (case_tac "ts @ [t]")
   apply simp+
   done
 
@@ -185,7 +185,7 @@
   apply simp
   apply (erule_tac x = "t \<degree> a" in allE)
   apply (erule_tac x = T in allE)
-  apply (erule_tac x = lista in allE)
+  apply (erule_tac x = list in allE)
   apply (erule impE)
    apply (erule conjE)
    apply (erule typing.App)