src/HOL/ex/ROOT.ML

--- a/src/HOL/ex/ROOT.ML	Thu Jun 11 12:50:20 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Jun 11 14:25:58 2009 +0200
@@ -14,11 +14,10 @@
   "Codegenerator_Pretty_Test",
   "NormalForm",
   "../NumberTheory/Factorization",
-  "Predicate_Compile"
+  "Predicate_Compile",
+  "Predicate_Compile_ex"
 ];
 
-setmp quick_and_dirty true use_thy "Predicate_Compile_ex";
-
 use_thys [
   "Numeral",
   "Higher_Order_Logic",