Replacing a local definition (in a hypothesis) by a global definition (axiom)

[Alexander van der Vekens]

Recently, I introduced a global definition for the "Ring of Integers" (see also https://groups.google.com/d/msg/metamath/S70pyqlnxvE/HeN-uzhhBwAJ):

  df-zring $a |- ZZring = ( CCfld |`s ZZ ) $

Currently, such a definition is used locally in many theorems as hypothesis, e,g.:

    zrhval.1 $e |- Z = ( CCfld |`s ZZ ) $.
    zrhval.2 $e |- L = ( ZRHom ` R ) $.
    zrhval $p |- L = U. ( Z RingHom R ) $=

Now I want to replace such local definitions by the global one, so that the previous example would become:

    zrhval.2 $e |- L = ( ZRHom ` R ) $.
    zrhval $p |- L = U. ( ZZring RingHom R ) $=

By removing the hypothesis, however, the proof of such a theorem becomes completely invalid! Is there a simple way to perform such a transformation easily ((almost) automatically at best)? Until now, I rewrote the complete proofs (which was acceptable since the proofs were not very long, but there are many theorems to be updated with much longer proofs...).

Alexander

[Alexander van der Vekens]

I tried the following with mmj2:

1. open the original theorem (with local definition)
2. copy proof into a text editor
3. delete the hypothesis containing the local definition
4. replace the local class variable (e.g. Z) by the globally defined symbol (e.g. ZZring)
5. create a new theorem
6. copy the modified proof
   
7. adjust the proof according to the erormessages provided after unification (these should not be a lot)
8. copy the new theorem (ncluding the proof) into set.mm
   

I think this is much better than retyping the complete prove. But is there even a better solution?

Alexander

[Benoit]

Maybe the proof is easier to modify when in explicit format ?  e.g. using

  > SAVE PROOF xxx / EXPLICIT / PACKED / FAST

and then copy-pasting

Benoit