src/HOL/Nominal/nominal_inductive2.ML
changeset 32172 c4e55f30d527
parent 32149 ef59550a55d3
child 32202 443d5cfaba1b
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 24 12:33:00 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 24 18:58:58 2009 +0200
     1.3 @@ -466,7 +466,7 @@
     1.4              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
     1.5            ctxt;
     1.6          val strong_inducts =
     1.7 -          ProjectRule.projects ctxt' (1 upto length names) strong_induct'
     1.8 +          Project_Rule.projects ctxt' (1 upto length names) strong_induct'
     1.9        in
    1.10          ctxt' |>
    1.11          LocalTheory.note Thm.generatedK