diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sat Aug 13 20:20:36 2011 +0200 @@ -179,8 +179,8 @@ var nodes = previous.nodes edits foreach { - case (name, Document.Node.Remove()) => - doc_edits += (name -> Document.Node.Remove()) + case (name, Document.Node.Clear()) => + doc_edits += (name -> Document.Node.Clear()) nodes -= name case (name, Document.Node.Edits(text_edits)) =>