src/Pure/Thy/export_theory.scala
changeset 68172 0f14cf9c632f
parent 68171 13162bb3a677
child 68173 7ed88a534bb6
     1.1 --- a/src/Pure/Thy/export_theory.scala	Sun May 13 20:04:59 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 13 20:24:33 2018 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  {
     1.5    /* entities */
     1.6  
     1.7 -  sealed case class Entity(name: String, kind: String, serial: Long, pos: Position.T)
     1.8 +  sealed case class Entity(name: String, serial: Long, pos: Position.T)
     1.9    {
    1.10      override def toString: String = name
    1.11    }
    1.12 @@ -23,10 +23,9 @@
    1.13      tree match {
    1.14        case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    1.15          val name = Markup.Name.unapply(props) getOrElse err()
    1.16 -        val kind = Markup.Kind.unapply(props) getOrElse err()
    1.17          val serial = Markup.Serial.unapply(props) getOrElse err()
    1.18          val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
    1.19 -        (Entity(name, kind, serial, pos), body)
    1.20 +        (Entity(name, serial, pos), body)
    1.21        case _ => err()
    1.22      }
    1.23    }