diff -r 642b6105e6f4 -r 7e119f32276a src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Wed Dec 28 17:02:38 2016 +0100
+++ b/src/Pure/General/codepoint.scala	Wed Dec 28 17:10:09 2016 +0100
@@ -25,7 +25,7 @@
 
   def length(s: String): Int = iterator(s).length
 
-  trait Length extends isabelle.Length
+  trait Length extends Text.Length
   {
     protected def codepoint_length(c: Int): Int = 1
 
@@ -34,7 +34,7 @@
 
     def offset(s: String, i: Int): Option[Text.Offset] =
     {
-      if (i <= 0 || s.forall(_ < 0x80)) isabelle.Length.offset(s, i)
+      if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i)
       else {
         val length = s.length
         var offset = 0