src/Pure/pure_syn.ML

--- a/src/Pure/pure_syn.ML	Thu Feb 27 17:24:46 2014 +0100
+++ b/src/Pure/pure_syn.ML	Thu Feb 27 17:29:58 2014 +0100
@@ -22,11 +22,11 @@
     "ML text from file"
     (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
         let
-          val [{src_path, text, pos}] = files (Context.theory_of gthy);
-          val provide = Thy_Load.provide (src_path, SHA1.digest text);
+          val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
+          val provide = Thy_Load.provide (src_path, digest);
         in
           gthy
-          |> ML_Context.exec (fn () => ML_Context.eval_text true pos text)
+          |> ML_Context.exec (fn () => ML_Context.eval_text true pos (cat_lines lines))
           |> Local_Theory.propagate_ml_env
           |> Context.mapping provide (Local_Theory.background_theory provide)
         end)));