module AmbiguousSymbol;

  axiom A : Type;

  module O;
    inductive T {
      A : T;
    };
  end;
  open O;

  module M;
    axiom A : Type;
  end;
  open M;

  axiom B : A;
end;