src/Provers/ind.ML
changeset 19299 5f0610aafc48
parent 15570 8d8c70b41bab
child 20344 d02b43ea722e
     1.1 --- a/src/Provers/ind.ML	Tue Mar 21 12:17:38 2006 +0100
     1.2 +++ b/src/Provers/ind.ML	Tue Mar 21 12:18:06 2006 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  fun all_frees_tac (var:string) i thm = 
     1.5      let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
     1.6          val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
     1.7 -        val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
     1.8 +        val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
     1.9      in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
    1.10  
    1.11  fun REPEAT_SIMP_TAC simp_tac n i =