src/HOL/Tools/record_package.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18858 ceb93f3af7f0
     1.1 --- a/src/HOL/Tools/record_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -1215,8 +1215,8 @@
     1.4  (* attributes *)
     1.5  
     1.6  fun case_names_fields x = RuleCases.case_names ["fields"] x;
     1.7 -fun induct_type_global name = [case_names_fields, Attrib.theory (InductAttrib.induct_type name)];
     1.8 -fun cases_type_global name = [case_names_fields, Attrib.theory (InductAttrib.cases_type name)];
     1.9 +fun induct_type_global name = [case_names_fields, InductAttrib.induct_type name];
    1.10 +fun cases_type_global name = [case_names_fields, InductAttrib.cases_type name];
    1.11  
    1.12  (* tactics *)
    1.13  
    1.14 @@ -1993,8 +1993,8 @@
    1.15      val final_thy =
    1.16        thms_thy
    1.17        |> (snd oo PureThy.add_thmss)
    1.18 -          [(("simps", sel_upd_simps), [Attrib.theory Simplifier.simp_add]),
    1.19 -           (("iffs",iffs), [Attrib.theory iff_add])]
    1.20 +          [(("simps", sel_upd_simps), [Simplifier.simp_add]),
    1.21 +           (("iffs",iffs), [iff_add])]
    1.22        |> put_record name (make_record_info args parent fields extension induct_scheme')
    1.23        |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
    1.24        |> add_record_equalities extension_id equality'