src/Provers/ind.ML
changeset 15570 8d8c70b41bab
parent 15462 b4208fbf9439
child 19299 5f0610aafc48
     1.1 --- a/src/Provers/ind.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Provers/ind.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -41,9 +41,9 @@
     1.4  (*Generalizes over all free variables, with the named var outermost.*)
     1.5  fun all_frees_tac (var:string) i thm = 
     1.6      let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
     1.7 -        val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
     1.8 +        val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
     1.9          val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
    1.10 -    in foldl (qnt_tac i) (all_tac,frees') thm end;
    1.11 +    in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
    1.12  
    1.13  fun REPEAT_SIMP_TAC simp_tac n i =
    1.14  let fun repeat thm =