# HG changeset patch
# User wenzelm
# Date 1232031079 -3600
# Node ID 2819ba5f0c32767f71d52073fc4a30387f72c746
# Parent  8f0a481199e7f7b90e3dcd9279f848718c2c4f7b
command 'Isar.edit_document': actually invoke edit_document;

diff -r 8f0a481199e7 -r 2819ba5f0c32 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Thu Jan 15 12:16:51 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Thu Jan 15 15:51:19 2009 +0100
@@ -256,7 +256,7 @@
 val _ =
   OuterSyntax.internal_command "Isar.edit_document"
     (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
-      >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => end_document id new_id edits)));
+      >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => edit_document id new_id edits)));
 
 end;