[isabelle] term_tvars



Hello,

I often need to investigate the instantiation of type variables in a proofterm.
The order in which this is done is that returned by the function
term_tvars : term -> (indexname * sort) list
This works fine when I extract a term from a proofterm, eg

ML {* val (_ %% (_ %% ((((((PAxm(_,x,_) % _) % _) % _) % _)%% _) %% _)) %% _) = get_proof "HOL.TrueI" *}
ML {* term_tvars x *}

val it = [(("'b", 0), ["logic"]), (("'a", 0), ["logic"])]
: (Term.indexname * Term.sort) list



However, when I construct a term myself, it doesn't

ML {* term_tvars (read "INTER") *}
val it = [] : (Term.indexname * Term.sort) list

even though this INTER has two free type variables.

How can I get this to work?

Thanks,

Sean







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