src/Pure/General/file.ML
changeset 73264 440546ea20e6
parent 72511 460d743010bc
child 73314 87403fde8cc3
--- a/src/Pure/General/file.ML	Sat Feb 20 22:09:16 2021 +0100
+++ b/src/Pure/General/file.ML	Sat Feb 20 23:01:35 2021 +0100
@@ -48,10 +48,10 @@
 val standard_path = Path.implode o Path.expand;
 val platform_path = ML_System.platform_path o standard_path;
 
-val bash_path = Bash_Syntax.string o standard_path;
-val bash_paths = Bash_Syntax.strings o map standard_path;
+val bash_path = Bash.string o standard_path;
+val bash_paths = Bash.strings o map standard_path;
 
-val bash_platform_path = Bash_Syntax.string o platform_path;
+val bash_platform_path = Bash.string o platform_path;
 
 
 (* full_path *)