src/HOL/Tools/Datatype/datatype.ML

 
 (* add_cases_induct *)
 
 fun add_cases_induct infos induction thy =
   let
-    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
+    val inducts = Project_Rule.projections (ProofContext.init thy) induction;
 
     fun named_rules (name, {index, exhaustion, ...}: info) =
       [((Binding.empty, nth inducts index), [Induct.induct_type name]),
        ((Binding.empty, exhaustion), [Induct.cases_type name])];
     fun unnamed_rule i =