# HG changeset patch
# User wenzelm
# Date 1574174741 -3600
# Node ID b1c555d3cd717a5f2c1c4c4bc69eaf170235efbc
# Parent  6046f203c245d752088f5f7a3521a7ad52453040
tuned signature -- more operations;

diff -r 6046f203c245 -r b1c555d3cd71 src/Pure/Thy/export.scala
--- 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 =