src/Pure/Thy/thy_syntax.scala

--- a/src/Pure/Thy/thy_syntax.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
+      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
       result()
     }
   }
@@ -226,7 +226,7 @@
         commands
       case cmd :: _ =>
         val hook = commands.prev(cmd)
-        val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
+        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }