tuned signature -- removed somewhat pointless operation;
authorwenzelm
Fri, 03 Aug 2018 20:14:13 +0200
changeset 68717 54a5043d4cd5
parent 68716 040c6298850b
child 68718 ce18a3924864
tuned signature -- removed somewhat pointless operation;
src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Aug 03 15:29:18 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Aug 03 20:14:13 2018 +0200
@@ -158,8 +158,6 @@
 
   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 =