# HG changeset patch # User wenzelm # Date 933972231 -7200 # Node ID a38dc0c6b2447a23821fd95bc0f8bf09acc8ef47 # Parent 5a80f69d6c625fdbc569f3694db456f4769f3e2e made SML happy; diff -r 5a80f69d6c62 -r a38dc0c6b244 src/Pure/Interface/proof_general.ML --- a/src/Pure/Interface/proof_general.ML Fri Aug 06 22:37:57 1999 +0200 +++ b/src/Pure/Interface/proof_general.ML Fri Aug 06 22:43:51 1999 +0200 @@ -101,7 +101,7 @@ (* messages *) val plain_output = std_output o suffix "\n"; -val plain_writeln = Library.setmp writeln_fn plain_output; +fun plain_writeln x = Library.setmp writeln_fn plain_output x; fun decorate_lines bg en "" = plain_output o enclose bg en | decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;