llist.ML

--- a/llist.ML	Tue Nov 30 17:44:04 1993 +0100
+++ b/llist.ML	Wed Dec 01 13:05:25 1993 +0100
@@ -99,8 +99,8 @@
     "LList_corec(a,f) <= case(f(a), %u.NIL, \
 \			   %v. split(v, %z w. CONS(z, LList_corec(w,f))))";
 by (rtac UN1_least 1);
-by (nat_ind_tac "k" 1);
-by (ALLGOALS(simp_tac corec_fun_ss));
+by (res_inst_tac [("n","k")] natE 1);
+by (ALLGOALS (asm_simp_tac corec_fun_ss));
 by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
 val LList_corec_subset1 = result();