[isabelle] Generating fresh type variables



Hello all,

I'm basically new to the ML part of Isabelle.

I'm defining a ML function to automatically generate specifications of an 
Isabelle function (these specifications are given as argument to 
Function_Fun.add_fun). During the generation, I obtain terms containing 
schematic type variables. I need to constrain (with sorts) the types appearing 
in these specifications, and I also transform the schematic type variables to 
type variables (I think I have to).

However when I use this function in a locale, my generated type variables can 
be the same as the locale's one (and a type capture occurs) which certainly 
means I'm doing something wrong. What is the correct way to generate fresh 
type variables (TFree) ?

I've searched through the Isabelle Cookbook and the sources 
(Pure/{type.ML,term.ML,Isar/*local*}) without any real clue. Have I to collect 
type variables of current locale fixed terms and use Name.variant ?

Thanks,

Mathieu




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