--- a/src/Pure/Isar/isar_document.ML Wed Jan 06 22:21:25 2010 +0100
+++ b/src/Pure/Isar/isar_document.ML Wed Jan 06 23:18:12 2010 +0100
@@ -232,11 +232,10 @@
in put_state state_id' state' end;
in (state_id', ((id, state_id'), make_state') :: updates) end;
-fun report_updates [] = ()
- | report_updates updates =
- implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
- |> Markup.markup Markup.assign
- |> Output.status;
+fun report_updates updates =
+ implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
+ |> Markup.markup Markup.assign
+ |> Output.status;
in