# HG changeset patch
# User wenzelm
# Date 1533302958 -7200
# Node ID 040c6298850bb3479ff57e33506f4520282d2dd1
# Parent  8197c285726717113a30d14515ab52daad9ec549
more operations;

diff -r 8197c2857267 -r 040c6298850b src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Aug 03 15:29:11 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Aug 03 15:29:18 2018 +0200
@@ -158,6 +158,8 @@
 
   sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
   {
+    def kind_name: (Kind.Value, String) = (kind, name)
+
     override def toString: String = kind.toString + quote(name)
 
     def cache(cache: Term.Cache): Entity =