considered removal of print_goals_ref;
authorwenzelm
Fri, 18 Jul 1997 13:51:28 +0200
changeset 3531 f6cc9112f4e9
parent 3530 d9ca80f0759c
child 3532 de271ba8086e
considered removal of print_goals_ref;
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;