src/Pure/Pure.thy

             Generated_Files.compile_generated_files_cmd
               (Toplevel.context_of st) args external export export_prefix source)));
 
 in end\<close>
 
+external_file "ROOT0.ML"
+external_file "ROOT.ML"
+
 
 subsection \<open>Embedded ML text\<close>
 
 ML \<open>
 local