diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/General/symbol.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -130,11 +130,11 @@
 
   def length(text: CharSequence): Int = iterator(text).length
 
-  object Length extends isabelle.Length
+  object Length extends Text.Length
   {
     def apply(text: String): Int = length(text)
     def offset(text: String, i: Int): Option[Text.Offset] =
-      if (i <= 0 || iterator(text).forall(s => s.length == 1)) isabelle.Length.offset(text, i)
+      if (i <= 0 || iterator(text).forall(s => s.length == 1)) Text.Length.offset(text, i)
       else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
       else None
   }