src/Provers/ind.ML
changeset 20344 d02b43ea722e
parent 19299 5f0610aafc48
child 20854 f9cf9e62d11c
     1.1 --- a/src/Provers/ind.ML	Sat Aug 05 14:52:58 2006 +0200
     1.2 +++ b/src/Provers/ind.ML	Sat Aug 05 14:55:09 2006 +0200
     1.3 @@ -26,9 +26,9 @@
     1.4  
     1.5  val _$(_$Var(a_ixname,aT)) = concl_of spec;
     1.6  
     1.7 -fun add_term_frees tsig =
     1.8 +fun add_term_frees thy =
     1.9  let fun add(tm, vars) = case tm of
    1.10 -	Free(v,T) => if Type.typ_instance tsig (T,aT) then v ins vars
    1.11 +	Free(v,T) => if Sign.typ_instance thy (T,aT) then v ins vars
    1.12  		     else vars
    1.13        | Abs (_,_,body) => add(body,vars)
    1.14        | rator$rand => add(rator, add(rand, vars))
    1.15 @@ -40,8 +40,7 @@
    1.16  
    1.17  (*Generalizes over all free variables, with the named var outermost.*)
    1.18  fun all_frees_tac (var:string) i thm = 
    1.19 -    let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
    1.20 -        val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
    1.21 +    let val frees = add_term_frees (Thm.theory_of_thm thm) (List.nth(prems_of thm,i-1),[var]);
    1.22          val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
    1.23      in Library.foldl (qnt_tac i) (all_tac,frees') thm end;
    1.24