Incorrect matching of operator bodies when instantiating theory.

[MM45]

EC complains about the internal_val (of the Subtype theory) having an incompatible body when trying to instantiate an inner Subtype clone with a local/top-level subtype clone when instantiating a theory. The following MWE captures the problem:

require import AllCore.
require Subtype.

theory W.

op p : int -> bool.

clone import Subtype as HAW with
  type T <- int,
    op P <- p.

end W.

theory X.

op p : int -> bool.

clone import Subtype as HAX with
  type T <- int,
    op P <- p.

(* !!! "operator `HAW.internal_val' body incompatible body" !!! *)
clone import W as WC with
  op p <- p,

  theory HAW <- HAX.

end X.

The above used to work, but now it gives the commented error upon cloning W and trying to instantiate the Subtype clone in W with the top-level Subtype clone (in X).