diff -r 220abde9962b -r c4e55f30d527 src/Tools/project_rule.ML
--- a/src/Tools/project_rule.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/Tools/project_rule.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -24,7 +24,7 @@
   val projections: Proof.context -> thm -> thm list
 end;
 
-functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
+functor Project_Rule(Data: PROJECT_RULE_DATA): PROJECT_RULE =
 struct
 
 fun conj1 th = th RS Data.conjunct1;