diff -r c451856129cd -r e2726211f834 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Tue Sep 18 17:20:40 2012 +0200
+++ b/src/Pure/General/position.scala	Tue Sep 18 19:33:45 2012 +0200
@@ -20,6 +20,12 @@
   val File = new Properties.String(Isabelle_Markup.FILE)
   val Id = new Properties.Long(Isabelle_Markup.ID)
 
+  val Def_Line = new Properties.Int(Isabelle_Markup.DEF_LINE)
+  val Def_Offset = new Properties.Int(Isabelle_Markup.DEF_OFFSET)
+  val Def_End_Offset = new Properties.Int(Isabelle_Markup.DEF_END_OFFSET)
+  val Def_File = new Properties.String(Isabelle_Markup.DEF_FILE)
+  val Def_Id = new Properties.Long(Isabelle_Markup.DEF_ID)
+
   object Line_File
   {
     def unapply(pos: T): Option[(Int, String)] =
@@ -30,6 +36,16 @@
       }
   }
 
+  object Def_Line_File
+  {
+    def unapply(pos: T): Option[(Int, String)] =
+      (pos, pos) match {
+        case (Def_Line(i), Def_File(name)) => Some((i, name))
+        case (_, Def_File(name)) => Some((1, name))
+        case _ => None
+      }
+  }
+
   object Range
   {
     def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
@@ -50,6 +66,15 @@
       }
   }
 
+  object Def_Id_Offset
+  {
+    def unapply(pos: T): Option[(Long, Text.Offset)] =
+      (pos, pos) match {
+        case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
+        case _ => None
+      }
+  }
+
   object Id_Range
   {
     def unapply(pos: T): Option[(Long, Text.Range)] =
@@ -59,16 +84,7 @@
       }
   }
 
-  private val purge_pos = Map(
-    Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE,
-    Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET,
-    Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET,
-    Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE,
-    Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID)
-
-  def purge(props: T): T =
-    for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
-      yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
+  def purge(props: T): T = props.filterNot(p => Isabelle_Markup.POSITION_PROPERTIES(p._1))
 
 
   /* here: inlined formal markup */