src/HOL/Tools/record_package.ML

   in (Term.add_typ_tfrees (T, env), T) end;
 
 (* attributes *)
 
 fun case_names_fields x = RuleCases.case_names ["fields"] x;
-fun induct_type_global name = [case_names_fields, InductAttrib.induct_type name];
-fun cases_type_global name = [case_names_fields, InductAttrib.cases_type name];
+fun induct_type_global name = [case_names_fields, Induct.induct_type name];
+fun cases_type_global name = [case_names_fields, Induct.cases_type name];
 
 (* tactics *)
 
 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));