src/Pure/ML/ml_file.ML

--- a/src/Pure/ML/ml_file.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ML/ml_file.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -13,7 +13,7 @@
         let
           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
           val provide = Resources.provide (src_path, digest);
-          val source = {delimited = true, text = cat_lines lines, range = (pos, pos)};
+          val source = Input.source true (cat_lines lines) (pos, pos);
           val flags = {SML = false, exchange = false, redirect = true, verbose = true};
         in
           gthy