src/Pure/General/file.ML
changeset 48446 8f611bc3650b
parent 44879 3b6613366dd7
child 48911 5debc3e4fa81
--- a/src/Pure/General/file.ML	Mon Jul 23 15:05:05 2012 +0200
+++ b/src/Pure/General/file.ML	Mon Jul 23 15:44:42 2012 +0200
@@ -45,11 +45,7 @@
 
 val platform_path = Path.implode o Path.expand;
 
-fun shell_quote s =
-  if exists_string (fn c => c = "'") s then
-    error ("Illegal single quote in path specification: " ^ quote s)
-  else enclose "'" "'" s;
-
+val shell_quote = enclose "'" "'";
 val shell_path = shell_quote o platform_path;