diff -r 2bfe5de2d1fa -r 130076a81b84 src/Provers/ind.ML
--- 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;