src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

 val learn_isarN = "learn_isar"
 val learn_atpN = "learn_atp"
 val relearn_isarN = "relearn_isar"
 val relearn_atpN = "relearn_atp"
 
-fun mash_home () = getenv "ISABELLE_SLEDGEHAMMER_MASH"
+fun mash_script () = Path.explode "$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py"
 fun mash_model_dir () =
-  getenv "ISABELLE_HOME_USER" ^ "/mash"
-  |> tap (Isabelle_System.mkdir o Path.explode)
+  Path.explode "$ISABELLE_HOME_USER/mash"
+  |> tap Isabelle_System.mkdir
 val mash_state_dir = mash_model_dir
-fun mash_state_file () = mash_state_dir () ^ "/state"
+fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
 
 
 (*** Isabelle helpers ***)
 
 fun meta_char c =

     val core =
       "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
       " --numberOfPredictions " ^ string_of_int max_suggs ^
       (if save then " --saveModel" else "")
     val command =
-      mash_home () ^ "/src/mash.py --quiet --outputDir " ^ mash_model_dir () ^
-      " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
+      Path.implode (mash_script ()) ^ " --quiet --outputDir " ^
+      Path.implode (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
+      " >& " ^ err_file
       |> tap (fn _ => trace_msg ctxt (fn () =>
              case try File.read (Path.explode err_file) of
                NONE => "Done"
              | SOME "" => "Done"
              | SOME s => "Error: " ^ elide_string 1000 s))

 
 fun str_of_query (parents, feats) =
   "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n"
 
 fun mash_CLEAR ctxt =
-  let val path = mash_model_dir () |> Path.explode in
+  let val path = mash_model_dir () in
     trace_msg ctxt (K "MaSh CLEAR");
     File.fold_dir (fn file => fn _ =>
                       try File.rm (Path.append path (Path.basic file)))
                   path NONE;
     ()

 
 val version = "*** MaSh 0.0 ***"
 
 fun load _ (state as (true, _)) = state
   | load ctxt _ =
-    let val path = mash_state_file () |> Path.explode in
+    let val path = mash_state_file () in
       (true,
        case try File.read_lines path of
          SOME (version' :: node_lines) =>
          let
            fun add_edge_to name parent =

         case dirty of
           SOME names =>
           (NONE, fold (append_entry o Graph.get_entry fact_G) names [])
         | NONE => (SOME (version ^ "\n"), Graph.fold append_entry fact_G [])
     in
-      write_file banner (entries, str_of_entry) (mash_state_file ());
+      write_file banner (entries, str_of_entry)
+                 (Path.implode (mash_state_file ()));
       trace_msg ctxt (fn () =>
           "Saved fact graph (" ^ graph_info fact_G ^
           (case dirty of
              SOME dirty =>
              "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"