--- a/src/HOL/ex/ROOT.ML Sat Mar 07 15:20:32 2009 +0100
+++ b/src/HOL/ex/ROOT.ML Sun Mar 08 15:25:28 2009 +0100
@@ -15,7 +15,8 @@
"Codegenerator",
"Codegenerator_Pretty",
"NormalForm",
- "../NumberTheory/Factorization"
+ "../NumberTheory/Factorization",
+ "Predicate_Compile"
];
use_thys [