--- a/src/HOL/Tools/record_package.ML Thu Oct 04 14:42:11 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Thu Oct 04 14:42:47 2007 +0200
@@ -1372,8 +1372,8 @@
(* 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 *)