tuned signature -- more operations;

--- a/src/Pure/Thy/export.scala	Mon Nov 18 15:00:48 2019 +0100
+++ b/src/Pure/Thy/export.scala	Tue Nov 19 15:45:41 2019 +0100
@@ -84,6 +84,8 @@
   {
     override def toString: String = name
 
+    def compound_name: String = Export.compound_name(theory_name, name)
+
     val name_elems: List[String] = explode_name(name)
 
     def name_extends(elems: List[String]): Boolean =