Remove capability of unqualified constants from kernel?

[phlegmaticprogrammer]

Initially unqualified constants were thought to be private to the local namespace, but I am not so sure that this is a good idea any more.

Making something private could probably be achieved by already existing means.

[phlegmaticprogrammer]

Unqualified constants are here to stay, they are just variables introduced by a context which is not on the main context thread (see #67).

[phlegmaticprogrammer]

Actually not so sure about this anymore, as currently all context constants seem to be qualified, except when doing namespace resolution.

[phlegmaticprogrammer]

I think the following kernel convention makes sense:

• constants introduced not on the main thread cannot be qualified
• constants introduced on the main thread may be qualified, and then are public, or they may be unqualified, and then are private

This will be implemented based on #67.

A different option would be to have only qualified context constants, but I think this would be awkward and could easily lead to misunderstandings (although it probably would not be inconsistent):

theory Foo

context
  let 'bar = 10'
  theorem '\Foo\bar = 10'
    ...

context
  let 'bar = 20'
  theorem '\Foo\bar = 20'

Here we would have two different conflicting theorems about the same object '\Foo\bar', and this looks like an inconsistency to the user. It's not really an inconsistency because '\Foo\bar' refers to two different objects in different contexts, but the notation '\Foo\bar' really suggests it is the same object.