Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/export_theory.scala
changeset 72708 0cc96d337e8f
parent 72691 2126cf946086
child 72847 9dda93a753b1 
--- a/src/Pure/Thy/export_theory.scala	Wed Nov 25 15:12:02 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala	Wed Nov 25 15:24:55 2020 +0100
@@ -192,7 +192,7 @@
       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
         val name = Markup.Name.unapply(props) getOrElse err()
         val xname = Markup.XName.unapply(props) getOrElse err()
-        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
+        val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID)
         val id = Position.Id.unapply(props)
         val serial = Markup.Serial.unapply(props) getOrElse err()
         (Entity(kind, name, xname, pos, id, serial), body)
isabelle