# HG changeset patch
# User wenzelm
# Date 1380450071 -7200
# Node ID 7e6a82c593f49f0d867dca1c06e570a6d2767032
# Parent  711104822c8e97a440a5122342e3ff6b48304e5d
made SML/NJ happy (NB: toplevel ML environment is unmanaged);

diff -r 711104822c8e -r 7e6a82c593f4 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Sun Sep 29 12:18:47 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sun Sep 29 12:21:11 2013 +0200
@@ -31,6 +31,7 @@
 datatype inference_policy =
   No_Inferences | Unchecked_Inferences | Checked_Inferences
 
+val prefix = Library.prefix
 val fact_name_of = prefix fact_prefix o ascii_of
 
 fun atp_of_format (THF (Polymorphic, _, _)) = dummy_thfN
@@ -262,7 +263,7 @@
 
 val encode_meta = Sledgehammer_MaSh.encode_str
 
-val include_base_name_of_fact = encode_meta o theory_name_of_fact
+fun include_base_name_of_fact x = encode_meta (theory_name_of_fact x)
 
 fun include_line base_name =
   "include('" ^ include_name ^ "/" ^ base_name ^ include_suffix ^ "').\n"
diff -r 711104822c8e -r 7e6a82c593f4 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sun Sep 29 12:18:47 2013 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Sun Sep 29 12:21:11 2013 +0200
@@ -31,6 +31,8 @@
 open Sledgehammer_Provers
 open Sledgehammer_Isar
 
+val prefix = Library.prefix
+
 val MaSh_IsarN = MaShN ^ "-Isar"
 val MaSh_ProverN = MaShN ^ "-Prover"
 val MeSh_IsarN = MeShN ^ "-Isar"
diff -r 711104822c8e -r 7e6a82c593f4 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sun Sep 29 12:18:47 2013 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Sun Sep 29 12:21:11 2013 +0200
@@ -275,3 +275,15 @@
   fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
 end;
 
+
+(* OS.FileSys *)
+
+structure OS =
+struct
+  open OS;
+  structure FileSys =
+  struct
+    open FileSys;
+    fun fileSize a = mk_int (FileSys.fileSize a);
+  end;
+end;