check_file: disallow current dir (typically "");

--- a/src/Pure/Thy/thy_load.ML	Tue Aug 27 11:07:01 2002 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Aug 27 11:07:54 2002 +0200
@@ -80,7 +80,12 @@
 
     fun find_dir dir =
       get_first (find_ext (Path.append dir path)) ml_exts;
-  in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end;
+
+    val paths =
+      if Path.is_current path then error "Bad file specification"
+      else if Path.is_basic path then ! load_path
+      else [Path.current];
+  in get_first find_dir paths end;
 
 
 (* load_file *)