src/HOL/HOLCF/Tools/Domain/domain_induction.ML

       fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
         let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
         in bot :: map name_of (#con_specs constr_info) end
     in adms @ flat (map2 one_eq bottoms constr_infos) end
 
-  val inducts = Project_Rule.projections (ProofContext.init_global thy) ind
+  val inducts = Project_Rule.projections (Proof_Context.init_global thy) ind
   fun ind_rule (dname, rule) =
       ((Binding.empty, rule),
        [Rule_Cases.case_names case_ns, Induct.induct_type dname])
 
 in