[Repost] Instantiating multiple theories simultaneously

[Michael Hohmuth <hohmuth@inf.tu-dresden.de>]

[ I am reposting this message because I did not receive a single reply
  to my first posting.  Maybe it got lost somewhere?  --m ]

Dear PVS experts,

I have written a number of specifications, formulated in a set of PVS
theories.  These specifications also contain a number of axioms that
express relationships various theories' elements.  Now I want to write
another set of theories that refine my specifications.  For this I'd
like to use PVS' new theory instantiations.  

However, it is unclear to me how my instantiations should be
expressed and how I best avoid all the theory-instantiation bugs that
Hendrik Tews has recently uncovered:  See PR#'s 757--760 in
http://pvs.csl.sri.com/cgi-bin/pvs/pvs-bug-list/pvs-bug-list?bugs=open&bugs=analyzed&originator=tews&dates=all&order=normal

Here is a simplified example of what I want to do:

  A : THEORY
  BEGIN
    a : int
  END A
  
  B : THEORY
  BEGIN
    IMPORTING A
    b : int
  
    ab : AXIOM a = b
  END B
  
  Aimplementation : THEORY
  BEGIN
    IMPORTING A{{a:=5}}
  END Aimplementation
  
  Bimplementation : THEORY
  BEGIN
    IMPORTING Aimplementation
    IMPORTING B{{b:=5}}
  END Bimplementation

With these specifications, PVS generates the following TCC for
Bimplementation:

  % Mapped-axiom TCC generated (at line 23, column 14) for  B{{ b := 5 }}
    % unfinished
  IMP_B_ab_TCC1: OBLIGATION a = 5;

where (according to show-expanded-sequent) "a" refers to "A.a", not
"Aimplementation.a", of course, rendering the TCC unprovable.

So my question is: How can I instantiate theories A and B
simultaneously such that I get a TCC obligation like
"Aimplementation.a = 5" (or "5 = 5")?

Thanks much in advance,
Michael
-- 
hohmuth@sax.de, hohmuth@inf.tu-dresden.de
http://home.pages.de/~hohmuth/