src/HOL/TPTP/MaSh_Export.thy

--- a/src/HOL/TPTP/MaSh_Export.thy	Mon Dec 03 23:43:49 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Mon Dec 03 23:43:52 2012 +0100
@@ -5,13 +5,23 @@
 header {* MaSh Exporter *}
 
 theory MaSh_Export
-imports Complex_Main
+imports
+  Main
+(*
+  "~/afp/thys/Jinja/J/TypeSafe"
+  "~/afp/thys/ArrowImpossibilityGS/Thys/Arrow_Order"
+  "~/afp/thys/FFT/FFT"
+  "~~/src/HOL/Auth/NS_Shared"
+  "~~/src/HOL/IMPP/Hoare"
+  "~~/src/HOL/Library/Fundamental_Theorem_Algebra"
+  "~~/src/HOL/Proofs/Lambda/StrongNorm"
+*)
 begin
 
 ML_file "mash_export.ML"
 
 sledgehammer_params
-  [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+  [provers = spass, max_relevant = 40, strict, dont_slice, type_enc = mono_native,
    lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
 
 ML {*
@@ -23,46 +33,51 @@
 val thy = @{theory List}
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
+val prefix = "/tmp/" ^ Context.theory_name thy ^ "/"
+*}
+
+ML {*
+Isabelle_System.mkdir (Path.explode prefix)
 *}
 
 ML {*
 if do_it then
-  generate_accessibility @{context} thy false "/tmp/mash_accessibility"
+  generate_accessibility @{context} thy false (prefix ^ "mash_accessibility")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_features @{context} prover thy false "/tmp/mash_features"
+  generate_features @{context} prover thy false (prefix ^ "mash_features")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies"
+  generate_isar_dependencies @{context} thy false (prefix ^ "mash_dependencies")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_commands @{context} params thy "/tmp/mash_commands"
+  generate_commands @{context} params thy (prefix ^ "mash_commands")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions"
+  generate_mepo_suggestions @{context} params thy 1024 (prefix ^ "mash_mepo_suggestions")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies"
+  generate_atp_dependencies @{context} params thy false (prefix ^ "mash_atp_dependencies")
 else
   ()
 *}