list_ind_tac -> list.induct_tac

--- a/IOA/example/Lemmas.ML	Thu Dec 01 17:35:03 1994 +0100
+++ b/IOA/example/Lemmas.ML	Fri Dec 02 10:26:59 1994 +0100
@@ -232,14 +232,14 @@
 
 (* Lists *)
 
-goal List.thy "(L @ (x#M)) ~= []";
-  by (list_ind_tac "L" 1);
+goal List.thy "(xs @ (y#ys)) ~= []";
+  by (list.induct_tac "xs" 1);
   by (simp_tac list_ss 1);
   by (asm_simp_tac list_ss 1);
 qed "append_cons";
 
-goal List.thy "(X ~= hd(L@M)) = (X ~= if(L = [], hd(M), hd(L)))";
-  by (list_ind_tac "L" 1);
+goal List.thy "(x ~= hd(xs@ys)) = (x ~= if(xs = [], hd(ys), hd(xs)))";
+  by (list.induct_tac "xs" 1);
   by (simp_tac list_ss 1);
   by (asm_full_simp_tac list_ss 1);
 qed "not_hd_append";