Thanks again Dmitriy,
it seems that my "fix" was too quick. Since sending my email yesterday I
worried already whether doing unification inside adhoc_overloading.ML is
such a good idea (since the unifier might inject schematic type
variables stemming from the internal generic theory data of ad
Cf. http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e
Dmitriy
On 23.11.2014 21:20, Christian Sternagel wrote:
*Moved from isabelle-users*
Thanks for the crucial hint Dmitriy!
Coming back to the original issue of Andreas, some explanation might
be in order.
What we did until now
