author | wenzelm |
Thu, 15 Jan 2009 00:48:45 +0100 | |
changeset 29487 | 06f4bb9fdb85 |
parent 29486 | 23a26d17adc0 |
child 29488 | 8fc3aeece219 |
--- a/src/Pure/Isar/isar_document.ML Thu Jan 15 00:44:19 2009 +0100 +++ b/src/Pure/Isar/isar_document.ML Thu Jan 15 00:48:45 2009 +0100 @@ -176,9 +176,6 @@ fun update_state tr state = Future.fork_deps [state] (fn () => (case Future.join state of NONE => NONE | SOME st => Toplevel.run_command tr st)); -fun update_entry (id, state_id) entries = - Symtab.map_entry - fun update_states old_document new_document = let val Document {entries = old_entries, ...} = old_document;