adapted to new PureThy.add_thms etc.;
authorwenzelm
Mon Mar 13 12:25:52 2000 +0100 (2000-03-13)
changeset 8420f37fd19476ca
parent 8419 4770b1a12a93
child 8421 7156b8e26a17
adapted to new PureThy.add_thms etc.;
src/Pure/Thy/thy_parse.ML
src/Pure/axclass.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Mar 13 12:25:16 2000 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Mar 13 12:25:52 2000 +0100
     1.3 @@ -375,7 +375,7 @@
     1.4      val (axms_defs, axms_names) =
     1.5        mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
     1.6    in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
     1.7 -       "\n\n|> (PureThy.add_defs o map Thm.no_attributes)\n" ^ axms_defs, axms_names)
     1.8 +       "\n\n|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))\n" ^ axms_defs, axms_names)
     1.9    end;
    1.10  
    1.11  val constaxiom_decls =
    1.12 @@ -554,8 +554,8 @@
    1.13    section "consts" "|> Theory.add_consts" const_decls,
    1.14    section "syntax" "|> Theory.add_modesyntax" syntax_decls,
    1.15    section "translations" "|> Theory.add_trrules" trans_decls,
    1.16 -  axm_section "rules" "|> (PureThy.add_axioms o map Thm.no_attributes)" axiom_decls,
    1.17 -  axm_section "defs" "|> (PureThy.add_defs o map Thm.no_attributes)" axiom_decls,
    1.18 +  axm_section "rules" "|> (#1 oo (PureThy.add_axioms o map Thm.no_attributes))" axiom_decls,
    1.19 +  axm_section "defs" "|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))" axiom_decls,
    1.20    section "oracle" "|> Theory.add_oracle" oracle_decl,
    1.21    axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    1.22    axm_section "axclass" "|> (#1 ooo AxClass.add_axclass)" axclass_decl,
     2.1 --- a/src/Pure/axclass.ML	Mon Mar 13 12:25:16 2000 +0100
     2.2 +++ b/src/Pure/axclass.ML	Mon Mar 13 12:25:52 2000 +0100
     2.3 @@ -268,22 +268,19 @@
     2.4        (map inclass super_classes @ map (int_axm o #2) axms, inclass class);
     2.5  
     2.6      (*declare axioms and rule*)
     2.7 -    val axms_thy =
     2.8 +    val (axms_thy, ([intro], [axioms])) =
     2.9        class_thy
    2.10        |> Theory.add_path bclass
    2.11        |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
    2.12 -      |> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
    2.13 -
    2.14 -    val intro = PureThy.get_thm axms_thy introN;
    2.15 -    val axioms = PureThy.get_thms axms_thy axiomsN;
    2.16 +      |>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
    2.17      val info = {super_classes = super_classes, intro = intro, axioms = axioms};
    2.18  
    2.19      (*store info*)
    2.20      val final_thy =
    2.21        axms_thy
    2.22 -      |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
    2.23 +      |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts))
    2.24        |> Theory.parent_path
    2.25 -      |> PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)]
    2.26 +      |> (#1 o PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)])
    2.27        |> put_axclass_info class info;
    2.28    in (final_thy, {intro = intro, axioms = axioms}) end;
    2.29