--- 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
--- 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,