diff -r caf9bc780c80 -r 6790126ab5f6 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Jan 20 04:53:59 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Sat Jan 21 23:02:14 2006 +0100
@@ -1215,8 +1215,8 @@
 (* attributes *)
 
 fun case_names_fields x = RuleCases.case_names ["fields"] x;
-fun induct_type_global name = [case_names_fields, Attrib.theory (InductAttrib.induct_type name)];
-fun cases_type_global name = [case_names_fields, Attrib.theory (InductAttrib.cases_type name)];
+fun induct_type_global name = [case_names_fields, InductAttrib.induct_type name];
+fun cases_type_global name = [case_names_fields, InductAttrib.cases_type name];
 
 (* tactics *)
 
@@ -1993,8 +1993,8 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [(("simps", sel_upd_simps), [Attrib.theory Simplifier.simp_add]),
-           (("iffs",iffs), [Attrib.theory iff_add])]
+          [(("simps", sel_upd_simps), [Simplifier.simp_add]),
+           (("iffs",iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme')
       |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
       |> add_record_equalities extension_id equality'