diff -r 8ac97f71369d -r b75ce99617c7 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Dec 22 00:29:12 2005 +0100
+++ b/src/FOL/IFOL.thy	Thu Dec 22 00:29:14 2005 +0100
@@ -143,6 +143,15 @@
 
 use "IFOL_lemmas.ML"
 
+ML {*
+structure ProjectRule = ProjectRuleFun
+(struct
+  val conjunct1 = thm "conjunct1";
+  val conjunct2 = thm "conjunct2";
+  val mp = thm "mp";
+end)
+*}
+
 use "fologic.ML"
 use "hypsubstdata.ML"
 setup hypsubst_setup