# HG changeset patch
# User haftmann
# Date 1232089503 -3600
# Node ID d1df1504ff5e21839d7c7712659caa1d1a1e7ef9
# Parent  8fd3c1c7f0cb6391b747051cacbe87779550d784# Parent  2cbc80397a170d99cb1f0f7e753e4edd59146371
merged

diff -r 2cbc80397a17 -r d1df1504ff5e src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Fri Jan 16 08:04:39 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Fri Jan 16 08:05:03 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;