diff -r 220abde9962b -r c4e55f30d527 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Jul 24 12:33:00 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Jul 24 18:58:58 2009 +0200
@@ -712,7 +712,7 @@
           map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
 
     val ctxt3 = if no_ind orelse coind then ctxt2 else
-      let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
+      let val inducts = cnames ~~ Project_Rule.projects ctxt2 (1 upto length cnames) induct'
       in
         ctxt2 |>
         LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),