| changeset 3531 | f6cc9112f4e9 |
| parent 2992 | 395686b418a4 |
| child 3547 | 977d58464d7f |
--- 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;