--- a/src/Pure/Pure.thy Sat Dec 05 11:49:04 2020 +0100 +++ b/src/Pure/Pure.thy Sat Dec 05 12:14:40 2020 +0100 @@ -168,6 +168,9 @@ in end\<close> +external_file "ROOT0.ML" +external_file "ROOT.ML" + subsection \<open>Embedded ML text\<close>