src/Pure/ML-Systems/poplogml.ML

--- a/src/Pure/ML-Systems/poplogml.ML	Mon Dec 11 19:05:20 2006 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Mon Dec 11 19:05:23 2006 +0100
@@ -378,3 +378,4 @@
 end;
 
 fun use_text _ _ txt = use_string txt;
+fun use_file _ _ name = use name;