src/HOL/HOL.thy
changeset 32172 c4e55f30d527
parent 32171 220abde9962b
child 32176 893614e2c35c
     1.1 --- a/src/HOL/HOL.thy	Fri Jul 24 12:33:00 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Jul 24 18:58:58 2009 +0200
     1.3 @@ -1390,7 +1390,7 @@
     1.4  text {* Rule projections: *}
     1.5  
     1.6  ML {*
     1.7 -structure ProjectRule = ProjectRuleFun
     1.8 +structure Project_Rule = Project_Rule
     1.9  (
    1.10    val conjunct1 = @{thm conjunct1}
    1.11    val conjunct2 = @{thm conjunct2}