explicit check for requirement;

--- a/src/Pure/General/file.ML	Sat Nov 27 15:45:20 2010 +0100
+++ b/src/Pure/General/file.ML	Sat Nov 27 15:58:36 2010 +0100
@@ -37,7 +37,11 @@
 
 val platform_path = Path.implode o Path.expand;
 
-val shell_quote = enclose "'" "'";
+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_path = shell_quote o platform_path;