# HG changeset patch
# User wenzelm
# Date 952946752 -3600
# Node ID f37fd19476ca7485ebbd3467821b8894c35589bf
# Parent  4770b1a12a934cc353e90992a749db3b3f032d4d
adapted to new PureThy.add_thms etc.;

diff -r 4770b1a12a93 -r f37fd19476ca src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Mar 13 12:25:16 2000 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Mar 13 12:25:52 2000 +0100
@@ -375,7 +375,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 Thm.no_attributes)\n" ^ axms_defs, axms_names)
+       "\n\n|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))\n" ^ axms_defs, axms_names)
   end;
 
 val constaxiom_decls =
@@ -554,8 +554,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 Thm.no_attributes)" axiom_decls,
-  axm_section "defs" "|> (PureThy.add_defs o map Thm.no_attributes)" axiom_decls,
+  axm_section "rules" "|> (#1 oo (PureThy.add_axioms o map Thm.no_attributes))" axiom_decls,
+  axm_section "defs" "|> (#1 oo (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" "|> (#1 ooo AxClass.add_axclass)" axclass_decl,
diff -r 4770b1a12a93 -r f37fd19476ca src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Mar 13 12:25:16 2000 +0100
+++ b/src/Pure/axclass.ML	Mon Mar 13 12:25:52 2000 +0100
@@ -268,22 +268,19 @@
       (map inclass super_classes @ map (int_axm o #2) axms, inclass class);
 
     (*declare axioms and rule*)
-    val axms_thy =
+    val (axms_thy, ([intro], [axioms])) =
       class_thy
       |> Theory.add_path bclass
       |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
-      |> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
-
-    val intro = PureThy.get_thm axms_thy introN;
-    val axioms = PureThy.get_thms axms_thy axiomsN;
+      |>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
     val info = {super_classes = super_classes, intro = intro, axioms = axioms};
 
     (*store info*)
     val final_thy =
       axms_thy
-      |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
+      |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts))
       |> Theory.parent_path
-      |> PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)]
+      |> (#1 o PureThy.add_thms [Thm.no_attributes (intro_name bclass, intro)])
       |> put_axclass_info class info;
   in (final_thy, {intro = intro, axioms = axioms}) end;