# HG changeset patch
# User wenzelm
# Date 869226688 -7200
# Node ID f6cc9112f4e9ce06fa2592f4eee9b86b08aa76a4
# Parent  d9ca80f0759c7fe17463bf97ddc895ed63920443
considered removal of print_goals_ref;

diff -r d9ca80f0759c -r f6cc9112f4e9 src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Jul 18 13:37:16 1997 +0200
+++ b/src/Pure/display.ML	Fri Jul 18 13:51:28 1997 +0200
@@ -205,7 +205,7 @@
   end;
 
 
-(*"hook" for user interfaces: allows print_goals to be replaced*)
+(*"hook" for user interfaces: allows print_goals to be replaced*)	(* FIXME remove!? *)
 val print_goals_ref = ref print_goals;
 
 end;