diff -r 56e91ac0f074 -r 0aa16bc2abdb src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Oct 20 12:52:56 1999 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Oct 20 15:22:56 1999 +0200
@@ -49,6 +49,16 @@
 
 (* ML command execution -- 'eval' *)
 
+local
+
+fun drop_last [] = []
+  | drop_last [x] = []
+  | drop_last (x :: xs) = x :: drop_last xs;
+
+val drop_last_char = implode o drop_last o explode;
+
+in
+
 fun use_text print verbose txt =
   let
     val in_buffer = ref (explode txt);
@@ -65,7 +75,7 @@
         [] => ()
       | _ => (PolyML.compiler (get, put) (); exec ()));
 
-    fun show_output () = print (implode (rev (! out_buffer)));
+    fun show_output () = print (drop_last_char (implode (rev (! out_buffer))));
   in
     exec () handle exn => (show_output (); raise exn);
     if verbose then show_output () else ()
@@ -83,17 +93,6 @@
 
 (** OS related **)
 
-local
-
-fun drop_last [] = []
-  | drop_last [x] = []
-  | drop_last (x :: xs) = x :: drop_last xs;
-
-val drop_last_char = implode o drop_last o explode;
-
-in
-
-
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and