diff --git a/thys/Buchi_Complementation/Complementation_Build.thy b/thys/Buchi_Complementation/Complementation_Build.thy
--- a/thys/Buchi_Complementation/Complementation_Build.thy
+++ b/thys/Buchi_Complementation/Complementation_Build.thy
@@ -1,27 +1,27 @@
 section \<open>Build and test exported program with MLton\<close>
 
 theory Complementation_Build
 imports Complementation_Final
 begin
 
 external_file \<open>code/Autool.mlb\<close>
 external_file \<open>code/Prelude.sml\<close>
 external_file \<open>code/Autool.sml\<close>
 
 compile_generated_files \<^marker>\<open>contributor Makarius\<close>
   \<open>code/Complementation.ML\<close> (in Complementation_Final)
   external_files
     \<open>code/Autool.mlb\<close>
     \<open>code/Prelude.sml\<close>
     \<open>code/Autool.sml\<close>
   export_files \<open>code/Complementation.sml\<close> and \<open>code/Autool\<close> (exe)
   where \<open>fn dir =>
     let
       val exec = Generated_Files.execute (dir + Path.basic "code");
       val _ = exec \<open>Prepare\<close> "mv Complementation.ML Complementation.sml";
-      val _ = exec \<open>Compilation\<close> (File.bash_path \<^path>\<open>$ISABELLE_MLTON\<close> ^
+      val _ = exec \<open>Compilation\<close> (\<^verbatim>\<open>"$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS \<close> ^
             " -profile time -default-type intinf Autool.mlb");
       val _ = exec \<open>Test\<close> "./Autool help";
     in () end\<close>
 
 end
\ No newline at end of file
diff --git a/thys/PAC_Checker/PAC_Checker_MLton.thy b/thys/PAC_Checker/PAC_Checker_MLton.thy
--- a/thys/PAC_Checker/PAC_Checker_MLton.thy
+++ b/thys/PAC_Checker/PAC_Checker_MLton.thy
@@ -1,34 +1,34 @@
 (*
   File:         PAC_Checker_MLton.thy
   Author:       Mathias Fleury, Daniela Kaufmann, JKU
   Maintainer:   Mathias Fleury, JKU
 *)
 theory PAC_Checker_MLton
   imports PAC_Checker_Synthesis
 begin
 
 export_code PAC_checker_l_impl PAC_update_impl PAC_empty_impl the_error is_cfailed is_cfound
   int_of_integer Del Add Mult nat_of_integer String.implode remap_polys_l_impl
   fully_normalize_poly_impl union_vars_poly_impl empty_vars_impl
   full_checker_l_impl check_step_impl CSUCCESS
   Extension hashcode_literal' version
   in SML_imp module_name PAC_Checker
   file_prefix "checker"
 
 text \<open>Here is how to compile it:\<close>
 compile_generated_files _
   external_files
     \<open>code/parser.sml\<close>
     \<open>code/pasteque.sml\<close>
     \<open>code/pasteque.mlb\<close>
   where \<open>fn dir =>
     let
       val exec = Generated_Files.execute (dir + Path.basic "code");
       val _ =
         exec \<open>Compilation\<close>
-          (File.bash_path \<^path>\<open>$ISABELLE_MLTON\<close> ^ " " ^
+          (\<^verbatim>\<open>"$ISABELLE_MLTON" $ISABELLE_MLTON_OPTIONS \<close> ^
             "-const 'MLton.safe false' -verbose 1 -default-type int64 -output pasteque " ^
             "-codegen native -inline 700 -cc-opt -O3 pasteque.mlb");
     in () end\<close>
 
 end
\ No newline at end of file