--- a/src/Provers/ind.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Provers/ind.ML Thu Apr 22 10:52:32 2004 +0200
@@ -41,7 +41,7 @@
(*Generalizes over all free variables, with the named var outermost.*)
fun all_frees_tac (var:string) i thm =
- let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
+ let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
in foldl (qnt_tac i) (all_tac,frees') thm end;