Theorems from instantiated modules

[johnyf]

The below behavior is observed with fd345f7 (provided the change 3527ca8#diff-61546a0d8846ae3815028403ccc975afL65 is applied first).

Exception: (Failure
  "We expected exactly one matching child in <AssumeProveNode> but got 0")
Backtrace: Raised at file "format.ml", line 185, characters 41-52
Called from file "format.ml", line 412, characters 8-33
Called from file "format.ml", line 427, characters 6-24

However, the module that causes this is B from below. (Module A is in the include paths, and is seen by sany.jar.) The issue seems to relate to instantiation of module A, because if I change the statements to either

Inst == INSTANCE Nat and Inst!Nat

or remove the BY statement, then the error disappears.

----------------------------- MODULE A -----------------------------------------
THEOREM SomeTheorem ==
    ASSUME TRUE
    PROVE TRUE
================================================================================

------------------------------- MODULE B ---------------------------------------
Inst == INSTANCE A

THEOREM
    ASSUME TRUE
    PROVE TRUE
BY Inst!SomeTheorem
================================================================================