src/HOL/TPTP/ATP_Theory_Export.thy

 open ATP_Theory_Export;
 *}
 
 ML {*
 val do_it = true (* false ### *); (* switch to "true" to generate the files *)
-val thy = @{theory Groups}; (* @{theory Complex_Main}; ### *)
+val thy = @{theory Nat}; (* @{theory Complex_Main}; ### *)
 val ctxt = @{context}
 *}
 
 ML {*
 if do_it then
-  "/tmp/mash_accessibility.out"
+  "/tmp/mash_sample_problem.out"
   |> generate_mash_accessibility_file_for_theory thy
 else
   ()
 *}
 
 ML {*
 if do_it then
+  "/tmp/mash_accessibility.out"
+  |> generate_mash_accessibility_file_for_theory thy false
+else
+  ()
+*}
+
+ML {*
+if do_it then
   "/tmp/mash_features.out"
-  |> generate_mash_feature_file_for_theory ctxt thy
+  |> generate_mash_feature_file_for_theory thy false
 else
   ()
 *}
 
 ML {*
 if do_it then
   "/tmp/mash_dependencies.out"
-  |> generate_mash_dependency_file_for_theory thy
+  |> generate_mash_dependency_file_for_theory thy false
 else
    ()
 *}
 
 ML {*