src/Pure/ML-Systems/polyml.ML

     fn () => brk (99999, 0), en);
 
 
 (* ML command execution -- 'eval' *)
 
-val use_string =
+val use_strings =
   let
     fun exec line =
       let
         val is_first = ref true;
 
         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;
 
     fun execs [] = ()