# HG changeset patch
# User wenzelm
# Date 1162924793 -3600
# Node ID df149b8c86b86133ec65518ca8996b676b9d962a
# Parent  abfdce60b371addd75e9ba499cac52f09987afba
removed obsolete print_state_hook;

diff -r abfdce60b371 -r df149b8c86b8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Nov 07 19:39:52 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 07 19:39:53 2006 +0100
@@ -33,7 +33,6 @@
   val prompt_state_fn: (state -> string) ref
   val print_state_context: state -> unit
   val print_state_default: bool -> state -> unit
-  val print_state_hook: (bool -> state -> unit) -> unit
   val print_state_fn: (bool -> state -> unit) ref
   val print_state: bool -> state -> unit
   val pretty_state: bool -> state -> Pretty.T list
@@ -222,13 +221,8 @@
 val print_state_context = Pretty.writelns o pretty_state_context;
 fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
 
-val print_state_hooks = ref ([]: (bool -> state -> unit) list);
-fun print_state_hook f = change print_state_hooks (cons f);
 val print_state_fn = ref print_state_default;
-
-fun print_state prf_only state =
- (List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks);
-  ! print_state_fn prf_only state);
+fun print_state prf_only state = ! print_state_fn prf_only state;