MMT/urtheories/source/subtypes.mmt needs building twice

[cmaeder]

Because theory Inhabitation is (textually) given after the theory PredicateSubtypes that includes Inhabitation the source files needs to be build twice. The first time error: unbound token: ! is reported for PredicateSubtypes (line 17, column 25 or char 553 in the source file)

Luckily, building all of urtheories (in alphabetical order) twice is sufficient. theory PLF (from lf.mmt) needs to be known before subtypes.mmt any way.

[cmaeder]

user: build [urtheories] mmt-omdoc  subtypes.mmt
archive: [source -> narration] /var/data/localmh/MathHub/MMT/urtheories/source/subtypes.mmt -> /var/data/localmh/MathHub/MMT/urtheories/narration/subtypes.omdoc
      error: unbound token: !
    error: invalid unit: http://cds.omdoc.org/urtheories?PredicateSubtypes?sub?type:  |- {A,P}{x:A}! (P x)→A|P INHABITABLE
user: build [urtheories] mmt-omdoc  subtypes.mmt finished

use "build urtheories -mmt-omdoc subtypes.mmt" to remove it first.

[cmaeder]

Meanwhile, I've moved the theory PredicateSubtypes to the end of the file, yet an error remains:

 archive: [source -> narration] /home/travis/build/KWARC/MMT/urtheories/source/subtypes.mmt -> /home/travis/build/KWARC/MMT/urtheories/narration/subtypes.omdoc

    error: invalid unit: http://cds.omdoc.org/urtheories?PredicateSubtypes?subA_subA?type:  |- {A,P,Q}({x}P x→Q x)→A|P⊆‍A|Q INHABITABLE

[cmaeder]

@florian-rabe This is actually a new error introduced by revision 3163 185c583 (as git bisect revealed)

[cmaeder]

fixed a while ago by florian