# HG changeset patch
# User blanchet
# Date 1354641150 -3600
# Node ID 136d5318b1fef2dbfd5a0f5353bb0ed17b765351
# Parent  b79803ee14f3df600d9365fd0f28bfbea63a559d
tuned MaSh exporter -- and don't make temp directories unless explicitly told so

diff -r b79803ee14f3 -r 136d5318b1fe src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Tue Dec 04 18:12:29 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Dec 04 18:12:30 2012 +0100
@@ -5,17 +5,7 @@
 header {* MaSh Exporter *}
 
 theory MaSh_Export
-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"
-*)
+imports Main
 begin
 
 ML_file "mash_export.ML"
@@ -30,7 +20,7 @@
 
 ML {*
 val do_it = false (* switch to "true" to generate the files *)
-val thys = [@{theory Main}] (* [@{theory Fundamental_Theorem_Algebra}] *)
+val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
 val dir = space_implode "__" (map Context.theory_name thys)
@@ -38,7 +28,10 @@
 *}
 
 ML {*
-Isabelle_System.mkdir (Path.explode prefix)
+if do_it then
+  Isabelle_System.mkdir (Path.explode prefix)
+else
+  ()
 *}
 
 ML {*