src/HOL/Isar_examples/W_correct.thy

--- a/src/HOL/Isar_examples/W_correct.thy	Tue Feb 22 21:49:34 2000 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Feb 22 21:50:02 2000 +0100
@@ -45,7 +45,7 @@
 proof -;
   assume "a |- e :: t";
   thus ?thesis (is "?P a e t");
-  proof (rule has_type.induct);     (* FIXME induct method *)
+  proof (induct a e t in set: has_type);
     fix a n;
     assume "n < length (a::typ list)";
     hence "n < length (map ($ s) a)"; by simp;