[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 
begin 
locale M1 = 
fixes getval::"'msg ⇒ 'val" 
begin 
end 


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


end 




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, 
H. 





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