| changeset 32172 | c4e55f30d527 |
| parent 32149 | ef59550a55d3 |
| child 32202 | 443d5cfaba1b |
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Jul 24 12:33:00 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Jul 24 18:58:58 2009 +0200 @@ -152,7 +152,7 @@ val meta_spec = thm "meta_spec"; fun projections rule = - ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule + Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule |> map (standard #> RuleCases.save rule); val supp_prod = thm "supp_prod";