# 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 =