changeset 32172 | c4e55f30d527 |
parent 31794 | 71af1fd6a5e4 |
child 33368 | b1cf34f1855c |
--- 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;