--- 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"), []),