# HG changeset patch
# User wenzelm
# Date 870871364 -7200
# Node ID 88a279998f907cb69b19a4bf2e29d34fa3730794
# Parent  aee7effe0816e296080738e5b41f0c57c2034d2e
renamed use_string to use_strings;

diff -r aee7effe0816 -r 88a279998f90 src/Pure/ML-Systems/MLWorks.ML
--- a/src/Pure/ML-Systems/MLWorks.ML	Wed Aug 06 14:35:52 1997 +0200
+++ b/src/Pure/ML-Systems/MLWorks.ML	Wed Aug 06 14:42:44 1997 +0200
@@ -84,7 +84,7 @@
 val tmpName = OS.FileSys.tmpName();
 
 (*Can one redirect 'use' directly to an instream?*)
-fun use_string slist =
+fun use_strings slist =
   let val tmpFile = TextIO.openOut tmpName
   in app (fn s => TextIO.output (tmpFile, s)) slist;
      TextIO.closeOut tmpFile;
diff -r aee7effe0816 -r 88a279998f90 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;
diff -r aee7effe0816 -r 88a279998f90 src/Pure/ML-Systems/smlnj-0.93.ML
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Wed Aug 06 14:35:52 1997 +0200
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Wed Aug 06 14:42:44 1997 +0200
@@ -30,34 +30,29 @@
 (* timing *)
 
 local
-
-(*print microseconds, suppressing trailing zeroes*)
-fun umakestring 0 = ""
-  | umakestring n =
-      chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
-
+  (*print microseconds, suppressing trailing zeroes*)
+  fun umakestring 0 = ""
+    | umakestring n =
+        chr (ord "0" + n div 100000) ^ umakestring (10 * (n mod 100000));
 in
-
-(*a conditional timing function: applies f to () and, if the flag is true,
-  prints its runtime*)
-
-fun cond_timeit flag f =
-  if flag then
-    let fun string_of_time (System.Timer.TIME {sec, usec}) =
-            makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
-        open System.Timer;
-        val start = start_timer()
-        val result = f();
-        val nongc = check_timer(start)
-        and gc = check_timer_gc(start);
-        val both = add_time(nongc, gc)
-    in  print("Non GC " ^ string_of_time nongc ^
-               "   GC " ^ string_of_time gc ^
-               "  both "^ string_of_time both ^ " secs\n");
-        result
-    end
-  else f();
-
+  (*a conditional timing function: applies f to () and, if the flag is true,
+    prints its runtime*)
+  fun cond_timeit flag f =
+    if flag then
+      let fun string_of_time (System.Timer.TIME {sec, usec}) =
+              makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
+          open System.Timer;
+          val start = start_timer()
+          val result = f();
+          val nongc = check_timer(start)
+          and gc = check_timer_gc(start);
+          val both = add_time(nongc, gc)
+      in  print("Non GC " ^ string_of_time nongc ^
+                 "   GC " ^ string_of_time gc ^
+                 "  both "^ string_of_time both ^ " secs\n");
+          result
+      end
+    else f();
 end;
 
 
@@ -81,7 +76,7 @@
 
 (* ML command execution *)
 
-fun use_string commands =
+fun use_strings commands =
   System.Compile.use_stream (open_string (implode commands));
 
 
diff -r aee7effe0816 -r 88a279998f90 src/Pure/ML-Systems/smlnj-1.09.ML
--- a/src/Pure/ML-Systems/smlnj-1.09.ML	Wed Aug 06 14:35:52 1997 +0200
+++ b/src/Pure/ML-Systems/smlnj-1.09.ML	Wed Aug 06 14:42:44 1997 +0200
@@ -80,7 +80,7 @@
 
 (* ML command execution *)
 
-val use_string = Compiler.Interact.useStream o TextIO.openString o implode;
+val use_strings = Compiler.Interact.useStream o TextIO.openString o implode;
 
 
 
diff -r aee7effe0816 -r 88a279998f90 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Aug 06 14:35:52 1997 +0200
+++ b/src/Pure/Thy/thm_database.ML	Wed Aug 06 14:42:44 1997 +0200
@@ -307,22 +307,22 @@
 
 fun bind_thm (name, thm) =
  (qed_thm := store_thm (name, (standard thm));
-  use_string ["val " ^ name ^ " = !qed_thm;"]);
+  use_strings ["val " ^ name ^ " = !qed_thm;"]);
 
 
 fun qed name =
  (qed_thm := store_thm (name, result ());
-  use_string ["val " ^ name ^ " = !qed_thm;"]);
+  use_strings ["val " ^ name ^ " = !qed_thm;"]);
 
 
 fun qed_goal name thy agoal tacsf =
  (qed_thm := store_thm (name, prove_goal thy agoal tacsf);
-  use_string ["val " ^ name ^ " = !qed_thm;"]);
+  use_strings ["val " ^ name ^ " = !qed_thm;"]);
 
 
 fun qed_goalw name thy rths agoal tacsf =
  (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf);
-  use_string ["val " ^ name ^ " = !qed_thm;"]);
+  use_strings ["val " ^ name ^ " = !qed_thm;"]);
 
 
 (** Retrieve theorems **)
diff -r aee7effe0816 -r 88a279998f90 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Wed Aug 06 14:35:52 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML	Wed Aug 06 14:42:44 1997 +0200
@@ -314,7 +314,7 @@
        save_data false;
 
        (*Store theory again because it could have been redefined*)
-       use_string
+       use_strings
          ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
 
        (*Add theory to list of all loaded theories (for index.html)