src/Pure/Isar/isar_document.ML

     (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
 
 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)));
-
-end;
-
-end;
-
+      >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => edit_document id new_id edits)));
+
+end;
+
+end;
+