diff -r 4bae781b8f7c -r cc06f5528bb1 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 16:48:46 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 17:07:05 2010 +0100
@@ -100,7 +100,7 @@
   /** text edits **/
 
   def text_edits(session: Session, previous: Document.Version,
-      edits: List[Document.Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
+      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -172,7 +172,7 @@
     /* resulting document edits */
 
     {
-      val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
+      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
       var nodes = previous.nodes
 
       edits foreach {