# HG changeset patch
# User wenzelm
# Date 916144781 -3600
# Node ID 78c068b838ffe8f69ffb613ab4a8e2e89a5a352f
# Parent  4d2d5556b4f9357781d5184e50f35e1a473315a9
eliminated Attribute structure;

diff -r 4d2d5556b4f9 -r 78c068b838ff src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Tue Jan 12 13:39:21 1999 +0100
+++ b/src/FOL/IFOL.ML	Tue Jan 12 13:39:41 1999 +0100
@@ -441,7 +441,7 @@
 
 local
 
-fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x;
+fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
 
 in
 
diff -r 4d2d5556b4f9 -r 78c068b838ff src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Jan 12 13:39:21 1999 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Tue Jan 12 13:39:41 1999 +0100
@@ -380,7 +380,7 @@
     val (axms_defs, axms_names) =
       mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
   in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
-       "\n\n|> (PureThy.add_defs o map Attribute.none)\n" ^ axms_defs, axms_names)
+       "\n\n|> (PureThy.add_defs o map Thm.no_attributes)\n" ^ axms_defs, axms_names)
   end;
 
 val constaxiom_decls =
@@ -571,8 +571,8 @@
   section "consts" "|> Theory.add_consts" const_decls,
   section "syntax" "|> Theory.add_modesyntax" syntax_decls,
   section "translations" "|> Theory.add_trrules" trans_decls,
-  axm_section "rules" "|> (PureThy.add_axioms o map Attribute.none)" axiom_decls,
-  axm_section "defs" "|> (PureThy.add_defs o map Attribute.none)" axiom_decls,
+  axm_section "rules" "|> (PureThy.add_axioms o map Thm.no_attributes)" axiom_decls,
+  axm_section "defs" "|> (PureThy.add_defs o map Thm.no_attributes)" axiom_decls,
   section "oracle" "|> Theory.add_oracle" oracle_decl,
   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,