diff -r 438adb97d82c -r 912f13865596 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jul 16 20:35:03 2020 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 16 22:24:03 2020 +0200
@@ -239,6 +239,7 @@
 ML_file "ML/ml_context.ML";
 ML_file "ML/ml_antiquotation.ML";
 ML_file "ML/ml_compiler2.ML";
+ML_file "ML/ml_pid.ML";
 
 
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";