src/Pure/ML-Systems/polyml.ML

--- a/src/Pure/ML-Systems/polyml.ML	Wed Aug 06 14:35:52 1997 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Aug 06 14:42:44 1997 +0200
@@ -42,7 +42,7 @@
 
 (* ML command execution -- 'eval' *)
 
-val use_string =
+val use_strings =
   let
     fun exec line =
       let
@@ -50,7 +50,7 @@
 
         fun get_line () =
           if ! is_first then (is_first := false; line)
-          else raise Io "use_string: buffer exhausted";
+          else raise Io "use_strings: buffer exhausted";
       in
         PolyML.compiler (get_line, print) ()
       end;