merged
authorwenzelm
Thu, 15 Jan 2009 15:51:50 +0100
changeset 29500 8fd3c1c7f0cb
parent 29498 49675edf127c (current diff)
parent 29499 2819ba5f0c32 (diff)
child 29503 d1df1504ff5e
child 29506 71f00a2c6dbd
child 29536 2de73447d47c
merged
--- a/src/Pure/Isar/isar_document.ML	Thu Jan 15 14:52:35 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Thu Jan 15 15:51:50 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;