--- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
@@ -18,6 +18,11 @@
*}
ML {*
+val do_it = true (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
+*}
+
+ML {*
if do_it then
generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
else
@@ -25,11 +30,6 @@
*}
ML {*
-val do_it = true (* switch to "true" to generate the files *);
-val thy = @{theory Nat}
-*}
-
-ML {*
if do_it then
generate_features thy false "/tmp/mash_features"
else