# HG changeset patch
# User wenzelm
# Date 1281038485 -7200
# Node ID d5d0af46f1ec67c1be085e7fa3baee5729047b91
# Parent  5c82435803341a23c39d452a5696f7c06811264f
tuned;

diff -r 5c8243580334 -r d5d0af46f1ec src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Thu Aug 05 21:56:38 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Thu Aug 05 22:01:25 2010 +0200
@@ -104,10 +104,10 @@
 fun edit_node (id, SOME id2) = insert_after id id2
   | edit_node (id, NONE) = delete_after id;
 
-fun edit_nodes (name, NONE) = Graph.del_node name
-  | edit_nodes (name, SOME edits) =
+fun edit_nodes (name, SOME edits) =
       Graph.default_node (name, empty_node) #>
-      Graph.map_node name (fold edit_node edits);
+      Graph.map_node name (fold edit_node edits)
+  | edit_nodes (name, NONE) = Graph.del_node name;
 
 
 
@@ -241,7 +241,7 @@
 in
 
 fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
-  NAMED_CRITICAL "Isar" (fn () => exception_trace (fn () =>
+  NAMED_CRITICAL "Isar" (fn () =>
     let
       val old_document = the_document old_id;
       val new_document = fold edit_nodes edits old_document;
@@ -264,7 +264,7 @@
       val _ = define_document new_id new_document';
       val _ = report_updates (flat updatess);
       val _ = execute new_document';
-    in () end));
+    in () end);
 
 end;