src/Pure/Thy/present.ML
changeset 37940 4857eab31298
parent 37939 965537d86fcc
child 38133 987680d2e77d
--- a/src/Pure/Thy/present.ML	Thu Jul 22 22:31:20 2010 +0200
+++ b/src/Pure/Thy/present.ML	Thu Jul 22 22:39:31 2010 +0200
@@ -466,7 +466,7 @@
         val base = Path.base path;
         val base_html = html_ext base;
         val _ = add_file (Path.append html_prefix base_html,
-          HTML.ml_file (Url.File base) (File.read path));
+          HTML.external_file (Url.File base) (File.read path));
       in (Url.File base_html, Url.File raw_path, loadit) end);
 
     fun prep_html_source (tex_source, html_source, html) =