# HG changeset patch
# User wenzelm
# Date 1636023688 -3600
# Node ID 84e5b4339db6384e9e7c5cb24e1bd57833482bc5
# Parent  b80a8d7db99ddd6396f2423232790f80f9521240
tuned -- eliminate clones stemming from d28a51dd9da6;

diff -r b80a8d7db99d -r 84e5b4339db6 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Nov 03 22:57:21 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Thu Nov 04 12:01:28 2021 +0100
@@ -182,18 +182,11 @@
     val DOCUMENT_HEADING = "document_heading"
     val DOCUMENT_TEXT = "document_text"
     val PROOF_TEXT = "proof_text"
-
-    def `export`(kind: String): String =
-      kind match {
-        case Markup.TYPE_NAME => TYPE
-        case Markup.CONSTANT => CONST
-        case _ => kind
-      }
   }
 
   def export_kind(kind: String): String =
-    if (kind == Markup.TYPE_NAME) "type"
-    else if (kind == Markup.CONSTANT) "const"
+    if (kind == Markup.TYPE_NAME) Kind.TYPE
+    else if (kind == Markup.CONSTANT) Kind.CONST
     else kind
 
   abstract class Content[T]
@@ -213,7 +206,7 @@
     serial: Long,
     content: Option[A])
   {
-    def export_kind: String = Kind.export(kind)
+    def export_kind: String = Export_Theory.export_kind(kind)
     override def toString: String = export_kind + " " + quote(name)
 
     def the_content: A =