--- 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;