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




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