- | i = index; IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
- G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular),i)
+ | IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
+ let attrs = `Provided, `Axiom, `Regular in
+ G.NObj (loc, N.Theorem (name, typ, None, attrs),i)