--- a/src/HOL/ex/Predicate_Compile.thy Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy Wed Sep 23 16:20:12 2009 +0200
@@ -1,6 +1,13 @@
theory Predicate_Compile
imports Complex_Main RPred
-uses "../Tools/Predicate_Compile/predicate_compile_core.ML"
+uses
+ "../Tools/Predicate_Compile/pred_compile_aux.ML"
+ "../Tools/Predicate_Compile/predicate_compile_core.ML"
+ "../Tools/Predicate_Compile/pred_compile_set.ML"
+ "../Tools/Predicate_Compile/pred_compile_data.ML"
+ "../Tools/Predicate_Compile/pred_compile_fun.ML"
+ "../Tools/Predicate_Compile/pred_compile_pred.ML"
+ "../Tools/Predicate_Compile/predicate_compile.ML"
begin
setup {* Predicate_Compile.setup *}