--- a/src/Pure/pure_syn.ML Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Pure/pure_syn.ML Sat Mar 01 22:46:31 2014 +0100
@@ -24,9 +24,10 @@
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
val provide = Thy_Load.provide (src_path, digest);
+ val source = {delimited = true, text = cat_lines lines, pos = pos};
in
gthy
- |> ML_Context.exec (fn () => ML_Context.eval_text true pos (cat_lines lines))
+ |> ML_Context.exec (fn () => ML_Context.eval_source true source)
|> Local_Theory.propagate_ml_env
|> Context.mapping provide (Local_Theory.background_theory provide)
end)));