src/Pure/ML/ml_file.ML

--- a/src/Pure/ML/ml_file.ML	Mon Jan 08 22:36:02 2018 +0100
+++ b/src/Pure/ML/ml_file.ML	Mon Jan 08 23:45:43 2018 +0100
@@ -19,9 +19,7 @@
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
 
-    val _ =
-      Thy_Output.check_comments (Toplevel.generic_theory_toplevel gthy)
-        (Input.source_explode source);
+    val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
 
     val flags =
       {SML = SML, exchange = false, redirect = true, verbose = true,