src/Provers/ind.ML
changeset 20854 f9cf9e62d11c
parent 20344 d02b43ea722e
     1.1 --- a/src/Provers/ind.ML	Wed Oct 04 14:14:33 2006 +0200
     1.2 +++ b/src/Provers/ind.ML	Wed Oct 04 14:17:38 2006 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  fun add_term_frees thy =
     1.6  let fun add(tm, vars) = case tm of
     1.7 -	Free(v,T) => if Sign.typ_instance thy (T,aT) then v ins vars
     1.8 +	Free(v,T) => if Sign.typ_instance thy (T,aT) then insert (op =) v vars
     1.9  		     else vars
    1.10        | Abs (_,_,body) => add(body,vars)
    1.11        | rator$rand => add(rator, add(rand, vars))