[mizar] Vocabulary name overloading

[Jeffrey Madsen <jmadsen@nd.edu>]

I came across a puzzling error in the following snippet of code:

definition
  let R be comRing;
  let I be Subset of Quot(R);
  attr I is invertible means
  :Def1:
  I * I" = rng NatHom Quot(R);
end;

definition
  let R be comRing;
  let I be Subset of R;
  attr I is invertible means
  :Def2:
  (NatHom Quot(R)) .: I is invertible;
end;

now
  let R be comRing;
  let I be Subset of R;
  assume I is invertible;
  then (NatHom Quot(R)) .: I is invertible by Def2;
::>                                         *4
end;

(NatHom Quot(R) has type "Function of R, Quot(R)".)

The error does not occur when I give the two definitions different names, but I'd like to use the same name for both. What's weird is there shouldn't be any conflict, because "Subset of R" does not widen to "Subset of Quot(R)" or vice versa. Can anyone see what I'm doing wrong?

Thanks,

Jeff