[isabelle] locale extension and type variables

Hi all, 

Here is the content of some test file (the output follows) to illustrate my problem: 

theory Test 
imports Main 
locale M1 = 
fixes getval::"'msg ⇒ 'val" 

locale M2 = M1 + 
fixes setval::"'val⇒'msg" 
begin end 
print_locale M1 
print_locale M2 


The first print_locale gives alright: 

locale M1 
fixes getval :: "'msg ⇒ 'val" 

But the second one gives: 

locale M2 
fixes getval :: "'a ⇒ 'b" 
and setval :: "'val ⇒ 'msg" 

What I would like is to have the same types in both of the two functions. I would like to get the following output: 

locale M2 
fixes getval :: "''val ⇒ 'msg" 
and setval :: "'val ⇒ 'msg" 

Any clue ? 
Thanks in advance, 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.