src/Pure/ML-Systems/poplogml.ML

   else pml_use name;
 
 end;
 
 fun use_text _ _ txt = use_string txt;
+fun use_file _ _ name = use name;