diff -r ad60214bef09 -r 440546ea20e6 src/Pure/General/file.ML
--- 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 *)