[isabelle-dev] type unification

Dmitriy Traytel traytel at in.tum.de
Thu Jul 11 07:57:58 CEST 2013

Hi Chris,

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


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 

More information about the isabelle-dev mailing list