src/Pure/Thy/thy_syntax.scala
changeset 43715 518e44a0ee15
parent 43697 77ce24aa1770
child 43722 9b5dadb0c28d
--- a/src/Pure/Thy/thy_syntax.scala	Sat Jul 09 12:56:51 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Jul 09 13:29:33 2011 +0200
@@ -194,7 +194,7 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Some(cmd_edits))
-          nodes += (name -> new Document.Node(node.header, commands2))
+          nodes += (name -> Document.Node(node.header, node.blobs, commands2))
       }
       (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
     }