В EBNF описании синтаксиса оберона имеем следующее:
## Код:
```
Module        = MODULE ident ";" [ImportList] DeclSeq [BEGIN StatementSeq] END ident ".".
```

Я правильно понимаю, что это описание синтаксиса не запрещает например такой исходник:
## Код:
```
MODULE A;
END B.
```

Т.е. о том что ident'ы должны быть одними и теми же мы просто описываем словами в спецификации языка.