diff -r 03232f0bb5c4 -r 46e053eda5dd src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Wed Aug 22 12:17:55 2012 +0200
+++ b/src/Pure/pure_syn.ML	Wed Aug 22 12:47:49 2012 +0200
@@ -19,8 +19,9 @@
   Outer_Syntax.command
     (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
     (Scan.ahead Parse.path -- Thy_Load.parse_files "ML_file"
-      >> (fn (src_path, files) => Toplevel.generic_theory (fn gthy =>
+      >> (fn (name, files) => Toplevel.generic_theory (fn gthy =>
         let
+          val src_path = Path.explode name;
           val (dir, [(txt, pos)]) = files (Context.theory_of gthy);
           val provide = Thy_Load.provide (src_path, (File.full_path dir src_path, SHA1.digest txt));
         in