(replaces Thy/parse.ML and Thy/syntax.ML) much simpler because of new theory extension functions; theory is now built up from an arbitrary list of definable 'sections'; new axclass and instance sections;