more operations;
authorwenzelm
Fri Aug 03 15:29:18 2018 +0200 (11 months ago)
changeset 68716040c6298850b
parent 68715 8197c2857267
child 68717 54a5043d4cd5
more operations;
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.scala	Fri Aug 03 15:29:11 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Fri Aug 03 15:29:18 2018 +0200
     1.3 @@ -158,6 +158,8 @@
     1.4  
     1.5    sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
     1.6    {
     1.7 +    def kind_name: (Kind.Value, String) = (kind, name)
     1.8 +
     1.9      override def toString: String = kind.toString + quote(name)
    1.10  
    1.11      def cache(cache: Term.Cache): Entity =