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