[isabelle-dev] type unification

[Christian Sternagel]

Dear list,

what is the proper way of obtaining a type from a term, in case I want 
to give it as argument to Sign.typ_unify (of Sign.typ_match for that 
matter)?

My question arises as follows. In adhoc_overloading.ML previously 
Sign.the_const_type was used to obtain the type of a constant. The 
result is a type with schematic type variables. Now that I want to use 
terms instead of constants (as strings) I replaced Sign.the_const_type 
by fastype_of, but this yields a type with fixed type variables and thus 
unification may fail. So once again: What is the proper way of getting a 
"schematic" type from a term?

cheers

chris