diff -r 26b95a6f3f79 -r bf31b35949ce src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -46,8 +46,8 @@
 proof -
   assume "a |- e :: t"
   thus ?thesis (is "?P a e t")
-  proof (induct (open) a e t)
-    case Var
+  proof induct
+    case (Var a n)
     hence "n < length (map ($ s) a)" by simp
     hence "map ($ s) a |- Var n :: map ($ s) a ! n"
       by (rule has_type.Var)
@@ -57,7 +57,7 @@
       by (simp only: app_subst_list)
     finally show "?P a (Var n) (a ! n)" .
   next
-    case Abs
+    case (Abs a e t1 t2)
     hence "$ s t1 # map ($ s) a |- e :: $ s t2"
       by (simp add: app_subst_list)
     hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
@@ -66,7 +66,7 @@
       by (simp add: app_subst_list)
   next
     case App
-    thus "?P a (App e1 e2) t1" by (simp add: has_type.App)
+    thus ?case by (simp add: has_type.App)
   qed
 qed