# HG changeset patch
# User wenzelm
# Date 1003766524 -7200
# Node ID 7099c865de3b7dbfff53eec5f1408cd01d19b883
# Parent  9a9da7969517ecedeb6f5742ce56956f735a4761
Display.print_current_goals_fn;

diff -r 9a9da7969517 -r 7099c865de3b src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Mon Oct 22 18:01:52 2001 +0200
+++ b/src/Pure/Interface/proof_general.ML	Mon Oct 22 18:02:04 2001 +0200
@@ -114,7 +114,7 @@
 (* theory / proof state output *)
 
 fun setup_state () =
- (current_goals_markers :=
+ (Display.current_goals_markers :=
     let
       val begin_state = oct_char "366";
       val end_state= oct_char "367";
@@ -192,7 +192,7 @@
 
 fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
 
-fun no_print_goals f = setmp print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
+fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
 
 fun repeat_undo 0 = ()
   | repeat_undo 1 = undo ()