[isabelle-dev] type unification

[Dmitriy Traytel]

Hi Chris,

I think Variable.polymorphic is what you want to use before using 
fastype_of.

Dmitriy

Am 11.07.2013 05:12, schrieb 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>