[isabelle-dev] type unification

Makarius makarius at sketis.net
Thu Aug 1 16:48:19 CEST 2013

On Thu, 11 Jul 2013, Christian Sternagel wrote:

> 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?

This perfectly normal Isabelle/ML user question is covered to some extent 
in the "implementation" manual, concerning Variable.polymorphic.

The reference in isabelle-dev style is
"The following example shows how to work with fixed term and type 
parameters and with type-inference."

Furthermore, to oral tradition of short Isabelle sayings has this entry 
about it:

   "A local context is characterized by a mixture of free and schematic
   variables.  Flipping coins via varify / unvarify only works in a global


More information about the isabelle-dev mailing list