# HG changeset patch
# User wenzelm
# Date 1117963893 -7200
# Node ID 2c05a7f662a3325ba05adb14de7b8c81fe33d1f9
# Parent  d978482479d34eb5c4987cc4f7b57e18c3c86947
tuned msg;

diff -r d978482479d3 -r 2c05a7f662a3 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Jun 05 11:31:32 2005 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sun Jun 05 11:31:33 2005 +0200
@@ -110,10 +110,12 @@
 local
 
 fun check_thy_aux (name, ml) =
-  (case check_file NONE (thy_path name) of
-    NONE => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
-      commas_quote (show_path ()))
-  | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE));
+  let val thy_file = thy_path name in
+    case check_file NONE thy_file of
+      NONE => error ("Could not find theory file " ^ quote (Path.pack thy_file) ^
+        " in dir(s) " ^ commas_quote (show_path ()))
+    | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
+  end;
 
 in