Re: [isabelle] term_tvars



Sean,

On Monday 24 October 2005 00:06, Sean McLaughlin wrote:
> ML {* term_tvars (read "INTER") *}
> val it = [] : (Term.indexname * Term.sort) list
>
> even though this INTER has two free type variables.

The result of  read "INTER"  has two TFree's, but no TVar's.  Consequently, 
term_tvars returns an empty list.  Use
  term_tfrees : Term.term -> (string * Term.sort) list
to obtain a list with all TFree's in a term.  See Pure/term.ML for further 
details.

Best regards,
Tjark





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.