[isabelle] type variable and locales extension

Hi all, 

There is something about type variables and locales extension that I do not understand. 

Here is 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 it to have the same types in both of the two functions ! I would like to read: 

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.