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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
