eliminated Attribute structure;
authorwenzelm
Tue Jan 12 13:39:41 1999 +0100 (1999-01-12)
changeset 609078c068b838ff
parent 6089 4d2d5556b4f9
child 6091 e3cdbd929a24
eliminated Attribute structure;
src/FOL/IFOL.ML
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/FOL/IFOL.ML	Tue Jan 12 13:39:21 1999 +0100
     1.2 +++ b/src/FOL/IFOL.ML	Tue Jan 12 13:39:41 1999 +0100
     1.3 @@ -441,7 +441,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x;
     1.8 +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
     1.9  
    1.10  in
    1.11  
     2.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Jan 12 13:39:21 1999 +0100
     2.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Jan 12 13:39:41 1999 +0100
     2.3 @@ -380,7 +380,7 @@
     2.4      val (axms_defs, axms_names) =
     2.5        mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
     2.6    in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
     2.7 -       "\n\n|> (PureThy.add_defs o map Attribute.none)\n" ^ axms_defs, axms_names)
     2.8 +       "\n\n|> (PureThy.add_defs o map Thm.no_attributes)\n" ^ axms_defs, axms_names)
     2.9    end;
    2.10  
    2.11  val constaxiom_decls =
    2.12 @@ -571,8 +571,8 @@
    2.13    section "consts" "|> Theory.add_consts" const_decls,
    2.14    section "syntax" "|> Theory.add_modesyntax" syntax_decls,
    2.15    section "translations" "|> Theory.add_trrules" trans_decls,
    2.16 -  axm_section "rules" "|> (PureThy.add_axioms o map Attribute.none)" axiom_decls,
    2.17 -  axm_section "defs" "|> (PureThy.add_defs o map Attribute.none)" axiom_decls,
    2.18 +  axm_section "rules" "|> (PureThy.add_axioms o map Thm.no_attributes)" axiom_decls,
    2.19 +  axm_section "defs" "|> (PureThy.add_defs o map Thm.no_attributes)" axiom_decls,
    2.20    section "oracle" "|> Theory.add_oracle" oracle_decl,
    2.21    axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    2.22    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,