src/Provers/ind.ML
changeset 14643 130076a81b84
parent 4452 b2ee34200dab
child 14772 c52060b69a8c
     1.1 --- a/src/Provers/ind.ML	Thu Apr 22 10:49:30 2004 +0200
     1.2 +++ b/src/Provers/ind.ML	Thu Apr 22 10:52:32 2004 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  (*Generalizes over all free variables, with the named var outermost.*)
     1.6  fun all_frees_tac (var:string) i thm = 
     1.7 -    let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
     1.8 +    let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
     1.9          val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
    1.10          val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
    1.11      in foldl (qnt_tac i) (all_tac,frees') thm end;