Display.print_current_goals_fn;
authorwenzelm
Mon, 22 Oct 2001 18:02:04 +0200
changeset 11888 7099c865de3b
parent 11887 9a9da7969517
child 11889 d9509f714982
Display.print_current_goals_fn;
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 ()