--- a/src/HOL/ex/ROOT.ML Thu Nov 20 19:06:05 2008 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Nov 20 19:43:34 2008 +0100
@@ -69,7 +69,7 @@
time_use_thy "PresburgerEx";
time_use_thy "Reflected_Presburger";
-time_use_thy "Reflection";
+use_thys ["Reflection", "ReflectionEx"];
time_use_thy "SVC_Oracle";