# HG changeset patch # User wenzelm # Date 1232031110 -3600 # Node ID 8fd3c1c7f0cb6391b747051cacbe87779550d784 # Parent 49675edf127c9ef932c7d548c44fd001c68cdf8d# Parent 2819ba5f0c32767f71d52073fc4a30387f72c746 merged diff -r 49675edf127c -r 8fd3c1c7f0cb src/Pure/Isar/isar_document.ML --- 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;