src/HOL/Isar_examples/W_correct.thy

 
 lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t";
 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;
     hence "map ($ s) a |- Var n :: map ($ s) a ! n";
       by (rule has_type.VarI);