# HG changeset patch
# User wenzelm
# Date 1614443522 -3600
# Node ID d01ca5e9e0daaf47c3be5d5b74526261315194e0
# Parent  87403fde8cc30780522e534378ed74a5ae3c6f63
tuned;

diff -r 87403fde8cc3 -r d01ca5e9e0da src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Sat Feb 27 17:25:54 2021 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Sat Feb 27 17:32:02 2021 +0100
@@ -29,7 +29,7 @@
 
 ML \<open>
 if do_it then
-  Isabelle_System.mkdir (Path.explode prob_dir)
+  ignore (Isabelle_System.make_directory (Path.explode prob_dir))
 else
   ()
 \<close>
diff -r 87403fde8cc3 -r d01ca5e9e0da src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Sat Feb 27 17:25:54 2021 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Sat Feb 27 17:32:02 2021 +0100
@@ -10,7 +10,7 @@
 
 ML \<open>
 if do_it then
-  Isabelle_System.mkdir (Path.explode prefix)
+  ignore (Isabelle_System.make_directory (Path.explode prefix))
 else
   ()
 \<close>
diff -r 87403fde8cc3 -r d01ca5e9e0da src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 27 17:25:54 2021 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sat Feb 27 17:32:02 2021 +0100
@@ -286,18 +286,14 @@
 
 fun generate_casc_lbt_isa_files_for_theory ctxt thy format infer_policy type_enc dir_name =
   let
-    val dir = Path.explode dir_name
-    val _ = Isabelle_System.mkdir dir
+    val dir = Isabelle_System.make_directory (Path.explode dir_name)
     val file_order_path = ap dir file_order_name
     val _ = File.write file_order_path ""
     val problem_order_path = ap dir problem_order_name
     val _ = File.write problem_order_path ""
-    val problem_dir = ap dir problem_name
-    val _ = Isabelle_System.mkdir problem_dir
-    val suggestion_dir = ap dir suggestion_name
-    val _ = Isabelle_System.mkdir suggestion_dir
-    val include_dir = ap problem_dir include_name
-    val _ = Isabelle_System.mkdir include_dir
+    val problem_dir = Isabelle_System.make_directory (ap dir problem_name)
+    val suggestion_dir = Isabelle_System.make_directory (ap dir suggestion_name)
+    val include_dir = Isabelle_System.make_directory (ap problem_dir include_name)
 
     val (facts, (prelude, groups)) =
       problem_of_theory ctxt thy format infer_policy type_enc