1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Tue Dec 04 18:12:29 2012 +0100
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Tue Dec 04 18:12:30 2012 +0100
     1.3 @@ -5,17 +5,7 @@
     1.4  header {* MaSh Exporter *}
     1.5  
     1.6  theory MaSh_Export
     1.7 -imports
     1.8 -  Main
     1.9 -(*
    1.10 -  "~/afp/thys/Jinja/J/TypeSafe"
    1.11 -  "~/afp/thys/ArrowImpossibilityGS/Thys/Arrow_Order"
    1.12 -  "~/afp/thys/FFT/FFT"
    1.13 -  "~~/src/HOL/Auth/NS_Shared"
    1.14 -  "~~/src/HOL/IMPP/Hoare"
    1.15 -  "~~/src/HOL/Library/Fundamental_Theorem_Algebra"
    1.16 -  "~~/src/HOL/Proofs/Lambda/StrongNorm"
    1.17 -*)
    1.18 +imports Main
    1.19  begin
    1.20  
    1.21  ML_file "mash_export.ML"
    1.22 @@ -30,7 +20,7 @@
    1.23  
    1.24  ML {*
    1.25  val do_it = false (* switch to "true" to generate the files *)
    1.26 -val thys = [@{theory Main}] (* [@{theory Fundamental_Theorem_Algebra}] *)
    1.27 +val thys = [@{theory List}]
    1.28  val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
    1.29  val prover = hd provers
    1.30  val dir = space_implode "__" (map Context.theory_name thys)
    1.31 @@ -38,7 +28,10 @@
    1.32  *}
    1.33  
    1.34  ML {*
    1.35 -Isabelle_System.mkdir (Path.explode prefix)
    1.36 +if do_it then
    1.37 +  Isabelle_System.mkdir (Path.explode prefix)
    1.38 +else
    1.39 +  ()
    1.40  *}
    1.41  
    1.42  ML {*