[isabelle-dev] type class instantiation

[Christian Sternagel]

Hi all,

it seems as if a recent change (in the repo version; within the last 2 
weeks, but I do not know exactly when) fixed the naming of type 
variables inside instantiations. To see what I mean:

I have a type "('f, 'v) term" for first-order terms with function 
symbols of type "'f" and variables of type "'v" and a type class "show" 
that provides a "shows_prec" and a "shows_list" function for efficient 
conversion into strings. To instantiate "term" I had (and this actually 
worked until recently)

instantiation "term" :: ("show", "show") "show" begin
   abbreviation "shows_term t ≡ shows_term' shows shows t"
   definition "shows_prec (d::nat) t = shows_term t"
   definition "shows_list_term (is::('f::show, 'v::show) term list) = 
shows_list_aux shows is"

   lemma assoc_term:
     "shows_prec d (t::('f::show, 'v::show) term) r @ s = shows_prec d t 
(r @ s)"
...

This no longer works and I'm forced to use "'a" and "'b" instead of "'f" 
and "'v". While this is not a severe restriction, I just wanted to know, 
whether this change was intentional (and as usual, it's reasons, just 
because I'm curious, not because I disagree to the change).

cheers

chris