# HG changeset patch
# User wenzelm
# Date 1231976925 -3600
# Node ID 06f4bb9fdb859fbf8aeeebb0fd08540122c67e33
# Parent  23a26d17adc01256aa6b8c830a98000c446fe549
removed junk;

diff -r 23a26d17adc0 -r 06f4bb9fdb85 src/Pure/Isar/isar_document.ML
--- 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;