# HG changeset patch
# User haftmann
# Date 1134115605 -3600
# Node ID 0e1d025d57b3a90ad1d37cf08d024e338268d8af
# Parent  2ef0183fa20b55886e4a50012b4441b285c7c4e4
oriented result pairs in PureThy

diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -262,7 +262,7 @@
   in
     thy2
     |> Theory.add_path (space_implode "_" new_type_names)
-    |> PureThy.add_thmss [(("recs", rec_thms), [])] |> Library.swap
+    |> PureThy.add_thmss [(("recs", rec_thms), [])]
     ||> Theory.parent_path
     |-> (fn thms => pair (reccomb_names, Library.flat thms))
   end;
@@ -439,7 +439,7 @@
   in
     thy'
     |> Theory.add_path big_name
-    |> PureThy.add_thmss [(("size", size_thms), [])] |> Library.swap
+    |> PureThy.add_thmss [(("size", size_thms), [])]
     ||> Theory.parent_path
     |-> (fn thmss => pair (Library.flat thmss))
   end;
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -81,21 +81,21 @@
 
 (* store theorems in theory *)
 
-fun store_thmss_atts label tnames attss thmss thy =
-  (thy, tnames ~~ attss ~~ thmss) |>
-  foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
-    Theory.add_path tname |>
-    (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
-    Theory.parent_path) |> Library.swap;
+fun store_thmss_atts label tnames attss thmss =
+  fold_map (fn ((tname, atts), thms) =>
+    Theory.add_path tname
+    #> PureThy.add_thmss [((label, thms), atts)]
+    #-> (fn thm::_ => Theory.parent_path #> pair thm)
+  ) (tnames ~~ attss ~~ thmss);
 
 fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
 
-fun store_thms_atts label tnames attss thms thy =
-  (thy, tnames ~~ attss ~~ thms) |>
-  foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
-    Theory.add_path tname |>
-    (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
-    Theory.parent_path) |> Library.swap;
+fun store_thms_atts label tnames attss thmss =
+  fold_map (fn ((tname, atts), thms) =>
+    Theory.add_path tname
+    #> PureThy.add_thms [((label, thms), atts)]
+    #-> (fn thm::_ => Theory.parent_path #> pair thm)
+  ) (tnames ~~ attss ~~ thmss);
 
 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
 
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -286,7 +286,7 @@
       
 fun add_rules simps case_thms size_thms rec_thms inject distinct
                   weak_case_congs cong_att =
-  (#1 o PureThy.add_thmss [(("simps", simps), []),
+  (snd o PureThy.add_thmss [(("simps", simps), []),
     (("", List.concat case_thms @ size_thms @ 
           List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
     (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
@@ -313,7 +313,7 @@
     fun unnamed_rule i =
       (("", proj i induction), [InductAttrib.induct_type_global ""]);
     val rules = List.concat (map named_rules infos) @ map unnamed_rule (length infos upto n - 1);
-  in #1 o PureThy.add_thms rules end;
+  in snd o PureThy.add_thms rules end;
 
 
 
@@ -533,11 +533,12 @@
 fun add_and_get_axioms_atts label tnames attss ts thy =
   foldr (fn (((tname, atts), t), (thy', axs)) =>
     let
-      val (thy'', [ax]) = thy' |>
-        Theory.add_path tname |>
-        PureThy.add_axioms_i [((label, t), atts)];
+      val ([ax], thy'') =
+        thy'
+        |> Theory.add_path tname
+        |> PureThy.add_axioms_i [((label, t), atts)];
     in (Theory.parent_path thy'', ax::axs)
-    end) (thy, []) (tnames ~~ attss ~~ ts);
+    end) (thy, []) (tnames ~~ attss ~~ ts) |> swap;
 
 fun add_and_get_axioms label tnames =
   add_and_get_axioms_atts label tnames (replicate (length tnames) []);
@@ -545,11 +546,12 @@
 fun add_and_get_axiomss label tnames tss thy =
   foldr (fn ((tname, ts), (thy', axss)) =>
     let
-      val (thy'', [axs]) = thy' |>
-        Theory.add_path tname |>
-        PureThy.add_axiomss_i [((label, ts), [])];
+      val ([axs], thy'') =
+        thy'
+        |> Theory.add_path tname
+        |> PureThy.add_axiomss_i [((label, ts), [])];
     in (Theory.parent_path thy'', axs::axss)
-    end) (thy, []) (tnames ~~ tss);
+    end) (thy, []) (tnames ~~ tss) |> swap;
 
 fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
     case_names_induct case_names_exhausts thy =
@@ -639,35 +641,35 @@
     val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
     val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2;
 
-    val (thy3, (([induct], [rec_thms]), inject)) =
-      thy2 |>
-      Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
-        [case_names_induct])] |>>>
-      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
-      (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
-      Theory.parent_path |>>>
-      add_and_get_axiomss "inject" new_type_names
-        (DatatypeProp.make_injs descr sorts);
+    val ((([induct], [rec_thms]), inject), thy3) =
+      thy2
+      |> Theory.add_path (space_implode "_" new_type_names)
+      |> PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
+          [case_names_induct])]
+      ||>> PureThy.add_axiomss_i [(("recs", rec_axs), [])]
+      ||> (if no_size then I else snd o PureThy.add_axiomss_i [(("size", size_axs), [])])
+      ||> Theory.parent_path
+      ||>> add_and_get_axiomss "inject" new_type_names
+            (DatatypeProp.make_injs descr sorts);
     val size_thms = if no_size then [] else get_thms thy3 (Name "size");
-    val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
+    val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
       (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
 
     val exhaust_ts = DatatypeProp.make_casedists descr sorts;
-    val (thy5, exhaustion) = add_and_get_axioms_atts "exhaust" new_type_names
+    val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names
       (map Library.single case_names_exhausts) exhaust_ts thy4;
-    val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
+    val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names
       (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
     val (split_ts, split_asm_ts) = ListPair.unzip
       (DatatypeProp.make_splits new_type_names descr sorts thy6);
-    val (thy7, split) = add_and_get_axioms "split" new_type_names split_ts thy6;
-    val (thy8, split_asm) = add_and_get_axioms "split_asm" new_type_names
+    val (split, thy7) = add_and_get_axioms "split" new_type_names split_ts thy6;
+    val (split_asm, thy8) = add_and_get_axioms "split_asm" new_type_names
       split_asm_ts thy7;
-    val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
+    val (nchotomys, thy9) = add_and_get_axioms "nchotomy" new_type_names
       (DatatypeProp.make_nchotomys descr sorts) thy8;
-    val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
+    val (case_congs, thy10) = add_and_get_axioms "case_cong" new_type_names
       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
-    val (thy11, weak_case_congs) = add_and_get_axioms "weak_case_cong" new_type_names
+    val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names
       (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
 
     val dt_infos = map (make_dt_info descr' sorts induct reccomb_names' rec_thms)
@@ -831,11 +833,12 @@
           [descr] sorts reccomb_names rec_thms thy8
       else ([], thy8);
 
-    val ([induction'], thy10) = thy9 |>
-      store_thmss "inject" new_type_names inject |> snd |>
-      store_thmss "distinct" new_type_names distinct |> snd |>
-      Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_thms [(("induct", induction), [case_names_induct])] |> Library.swap;
+    val ((_, [induction']), thy10) =
+      thy9
+      |> store_thmss "inject" new_type_names inject
+      ||>> store_thmss "distinct" new_type_names distinct
+      ||> Theory.add_path (space_implode "_" new_type_names)
+      ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
 
     val dt_infos = map (make_dt_info descr sorts induction' reccomb_names rec_thms)
       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -226,9 +226,10 @@
         val def_name = (Sign.base_name cname) ^ "_def";
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
           (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
-        val ([def_thm], thy') = thy |>
-          Theory.add_consts_i [(cname', constrT, mx)] |>
-          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
+        val ([def_thm], thy') =
+          thy
+          |> Theory.add_consts_i [(cname', constrT, mx)]
+          |> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
 
       in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
 
@@ -639,10 +640,11 @@
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]));
 
-    val (thy7, [dt_induct']) = thy6 |>
-      Theory.add_path big_name |>
-      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
-      Theory.parent_path;
+    val ([dt_induct'], thy7) =
+      thy6
+      |> Theory.add_path big_name
+      |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
+      ||> Theory.parent_path;
 
   in
     ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -451,13 +451,13 @@
     fun cases_spec name elim thy =
       thy
       |> Theory.add_path (Sign.base_name name)
-      |> (fst o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
+      |> (snd o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
       |> Theory.parent_path;
     val cases_specs = if no_elim then [] else map2 cases_spec names elims;
 
     val induct_att =
       if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
-    fun induct_spec (name, th) = #1 o PureThy.add_thms
+    fun induct_spec (name, th) = snd o PureThy.add_thms
       [(("", RuleCases.save induct th), [induct_att name])];
     val induct_specs =
       if no_induct then [] else map induct_spec (project_rules names induct);
@@ -794,16 +794,17 @@
         (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
       else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
 
-    val (thy2, intrs') =
-      thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
-    val (thy3, ([_, elims'], [induct'])) =
+    val (intrs', thy2) =
+      thy1
+      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
+    val (([_, elims'], [induct']), thy3) =
       thy2
       |> PureThy.add_thmss
         [(("intros", intrs'), []),
           (("elims", elims), [RuleCases.consumes 1])]
-      |>>> PureThy.add_thms
+      ||>> PureThy.add_thms
         [((coind_prefix coind ^ "induct", rulify (#1 induct)), #2 induct)]
-      |>> Theory.parent_path;
+      ||> Theory.parent_path;
   in (thy3,
     {defs = fp_def :: rec_sets_defs,
      mono = mono,
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -255,11 +255,11 @@
       commas_quote (map fst nameTs1) ^ " ...");
     val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t
         (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
-    val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
+    val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     val thy''' = thy''
-      |> (#1 o PureThy.add_thmss [(("simps", simps'),
+      |> (snd o PureThy.add_thmss [(("simps", simps'),
            [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
-      |> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
+      |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
       |> Theory.parent_path
   in
     (thy''', simps')
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -245,11 +245,11 @@
     val simp_att = if null tcs then
       [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
 
-    val (thy, (simps' :: rules', [induct'])) =
+    val ((simps' :: rules', [induct']), thy) =
       thy
       |> Theory.add_path bname
       |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
-      |>>> PureThy.add_thms [(("induct", induct), [])];
+      ||>> PureThy.add_thms [(("induct", induct), [])];
     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy
@@ -274,11 +274,11 @@
 
     val (thy1, congs) = thy |> app_thms raw_congs;
     val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
-    val (thy3, [induct_rules']) =
+    val ([induct_rules'], thy3) =
       thy2
       |> Theory.add_path bname
       |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
-      |>> Theory.parent_path;
+      ||> Theory.parent_path;
   in (thy3, {induct_rules = induct_rules'}) end;
 
 val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -1282,7 +1282,7 @@
              (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV NONE
              (Tactic.rtac UNIV_witness 1))
     val rewrite_rule = Tactic.rewrite_rule [def, rec_UNIV_I, rec_True_simp];
-  in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct])
+  in (map rewrite_rule [abs_inject, abs_inverse, abs_induct], thy')
   end;
 
 fun mixit convs refls =
@@ -1348,10 +1348,11 @@
     fun mk_defs () =
       thy
         |> extension_typedef name repT (alphas@[zeta])
-        |>> Theory.add_consts_i
+        ||> Theory.add_consts_i
               (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
-        |>>> (PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs)) #> Library.swap)
-        |>>> (PureThy.add_defs_i false (map Thm.no_attributes upd_specs) #> Library.swap)
+        ||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
+        ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
+        |> swap
     val (defs_thy, (([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs),upd_defs)) =
         timeit_msg "record extension type/selector/update defs:" mk_defs;
 
@@ -1500,8 +1501,8 @@
                 REPEAT (etac meta_allE 1), atac 1]);
     val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
 
-    val (thm_thy,([inject',induct',cases',surjective',split_meta'],
-                  [dest_convs',upd_convs'])) =
+    val (([inject',induct',cases',surjective',split_meta'], [dest_convs',upd_convs']),
+      thm_thy) =
       defs_thy
       |> (PureThy.add_thms o map Thm.no_attributes)
            [("ext_inject", inject),
@@ -1509,7 +1510,7 @@
             ("ext_cases", cases),
             ("ext_surjective", surjective),
             ("ext_split", split_meta)]
-      |>>> (PureThy.add_thmss o map Thm.no_attributes)
+      ||>> (PureThy.add_thmss o map Thm.no_attributes)
               [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)]
 
   in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
@@ -1740,7 +1741,6 @@
             ([],[],field_tr's, [])
         |> Theory.add_advanced_trfuns
             ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
-
         |> Theory.parent_path
         |> Theory.add_tyabbrs_i recordT_specs
         |> Theory.add_path bname
@@ -1748,10 +1748,11 @@
             (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
         |> (Theory.add_consts_i o map Syntax.no_syn)
             (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
-        |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs #> Library.swap)
-        |>>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs #> Library.swap)
-        |>>> ((PureThy.add_defs_i false o map Thm.no_attributes)
-               [make_spec, fields_spec, extend_spec, truncate_spec] #> Library.swap)
+        |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
+        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
+        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
+               [make_spec, fields_spec, extend_spec, truncate_spec])
+        |> swap
     val (defs_thy,((sel_defs,upd_defs),derived_defs)) =
         timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
          mk_defs;
@@ -1967,9 +1968,8 @@
       end);
      val equality = timeit_msg "record equality proof:" equality_prf;
 
-    val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
-                    derived_defs'],
-                   [surjective',equality']),[induct_scheme',induct',cases_scheme',cases'])) =
+    val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
+            [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
       defs_thy
       |> (PureThy.add_thmss o map Thm.no_attributes)
          [("select_convs", sel_convs_standard),
@@ -1978,10 +1978,10 @@
           ("update_defs", upd_defs),
           ("splits", [split_meta_standard,split_object,split_ex]),
           ("defs", derived_defs)]
-      |>>> (PureThy.add_thms o map Thm.no_attributes)
+      ||>> (PureThy.add_thms o map Thm.no_attributes)
           [("surjective", surjective),
            ("equality", equality)]
-      |>>> PureThy.add_thms
+      ||>> PureThy.add_thms
         [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
          (("induct", induct), induct_type_global name),
          (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
@@ -1992,7 +1992,7 @@
     val iffs = [ext_inject]
     val final_thy =
       thms_thy
-      |> (#1 oo PureThy.add_thmss)
+      |> (snd oo PureThy.add_thmss)
           [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
            (("iffs",iffs), [iff_add_global])]
       |> put_record name (make_record_info args parent fields extension induct_scheme')
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -49,7 +49,7 @@
         let
             fun process [] (thy,tm) =
                 let
-                    val (thy',thms) = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
+                    val (thms, thy') = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
                 in
                     (thy',hd thms)
                 end
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -159,14 +159,14 @@
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])
       |> add_def def (Logic.mk_defpair (setC, set))
-      ||>> (PureThy.add_axioms_i [((typedef_name, typedef_prop),
-          [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] #> Library.swap)
+      ||>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
+          [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
       ||> Theory.add_finals_i false [RepC, AbsC]
       |-> (fn (set_def, [type_definition]) => fn theory' =>
         let
           fun make th = Drule.standard (th OF [type_definition]);
-          val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
-              Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
+          val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
+              Rep_cases, Abs_cases, Rep_induct, Abs_induct], theory'') =
             theory'
             |> Theory.add_path name
             |> PureThy.add_thms
@@ -183,7 +183,7 @@
                   [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
                 ((Abs_name ^ "_induct", make Abs_induct),
                   [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
-            |>> Theory.parent_path;
+            ||> Theory.parent_path;
           val result = {type_definition = type_definition, set_def = set_def,
             Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
             Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOLCF/domain/axioms.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -111,7 +111,7 @@
     [take_def, finite_def])
 end; (* let *)
 
-fun add_axioms_i x = #1 o PureThy.add_axioms_i (map Thm.no_attributes x);
+fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x);
 fun add_axioms_infer axms thy = add_axioms_i (infer_types thy axms) thy;
 
 fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOLCF/domain/extender.ML
--- a/src/HOLCF/domain/extender.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOLCF/domain/extender.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -134,7 +134,7 @@
   in
     theorems_thy
     |> Theory.add_path (Sign.base_name comp_dnam)
-    |> (#1 o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
+    |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
     |> Theory.parent_path
   end;
 
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOLCF/domain/theorems.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -353,7 +353,7 @@
                         (List.filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
 val copy_rews = copy_strict::copy_apps @ copy_stricts;
 in thy |> Theory.add_path (Sign.base_name dname)
-       |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
+       |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
 		("iso_rews" , iso_rews  ),
 		("exhaust"  , [exhaust] ),
 		("casedist" , [casedist]),
@@ -368,7 +368,7 @@
 		("inverts" , inverts ),
 		("injects" , injects ),
 		("copy_rews", copy_rews)])))
-       |> (#1 o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
+       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
        |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
                  pat_rews @ dist_les @ dist_eqs @ copy_rews)
 end; (* let *)
@@ -630,7 +630,7 @@
 end; (* local *)
 
 in thy |> Theory.add_path comp_dnam
-       |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
+       |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
 		("take_rews"  , take_rews  ),
 		("take_lemmas", take_lemmas),
 		("finites"    , finites    ),
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOLCF/fixrec_package.ML
--- a/src/HOLCF/fixrec_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOLCF/fixrec_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -120,7 +120,7 @@
         in (n^"_unfold", thmL) :: unfolds ns thmR end;
     val unfold_thms = unfolds names ctuple_unfold_thm;
     val thms = ctuple_induct_thm :: unfold_thms;
-    val (thy'', _) = PureThy.add_thms (map Thm.no_attributes thms) thy';
+    val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy';
   in
     (thy'', names, fixdef_thms, map snd unfold_thms)
   end;
@@ -247,13 +247,13 @@
     if strict then let (* only prove simp rules if strict = true *)
       val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts);
       val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks));
-      val (thy'', simp_thms) = PureThy.add_thms simps thy';
+      val (simp_thms, thy'') = PureThy.add_thms simps thy';
       
       val simp_names = map (fn name => name^"_simps") cnames;
       val simp_attribute = rpair [Simplifier.simp_add_global];
       val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
     in
-      (#1 o PureThy.add_thmss simps') thy''
+      (snd o PureThy.add_thmss simps') thy''
     end
     else thy'
   end;
@@ -283,7 +283,7 @@
     val ts = map (prep_term thy) strings;
     val simps = map (fix_pat thy) ts;
   in
-    (#1 o PureThy.add_thmss [((name, simps), atts)]) thy
+    (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   end;
 
 val add_fixpat = gen_add_fixpat Sign.read_term Attrib.global_attribute;
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -111,7 +111,7 @@
       let
         val admissible' = option_fold_rule set_def admissible;
         val cpo_thms = [type_def, less_def, admissible'];
-        val (theory', _) =
+        val (_, theory') =
           theory
           |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"])
             (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
@@ -123,14 +123,14 @@
               (("lub_"     ^ name, typedef_lub     OF cpo_thms), []),
               (("thelub_"  ^ name, typedef_thelub  OF cpo_thms), []),
               (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
-          |>> Theory.parent_path;
+          ||> Theory.parent_path;
       in (theory', defs) end;
 
     fun make_pcpo UUmem (theory, defs as (type_def, less_def, set_def)) =
       let
         val UUmem' = option_fold_rule set_def UUmem;
         val pcpo_thms = [type_def, less_def, UUmem'];
-        val (theory', _) =
+        val (_, theory') =
           theory
           |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"])
             (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
@@ -141,7 +141,7 @@
               ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
               ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
               ])
-          |>> Theory.parent_path;
+          ||> Theory.parent_path;
       in (theory', defs) end;
     
     fun pcpodef_result (theory, UUmem_admissible) =
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/Isar/calculation.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -135,7 +135,7 @@
     ("sym", sym_attr, "declaration of symmetry rule"),
     ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
       "resolution with symmetry rule")],
-  #1 o PureThy.add_thms
+  snd o PureThy.add_thms
    [(("", transitive_thm), [trans_add_global]),
     (("", symmetric_thm), [sym_add_global])]];
 
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/Isar/context_rules.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -252,7 +252,7 @@
 end;
 
 val _ = Context.add_setup
-  [#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
+  [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
 
 
 (* low-level modifiers *)
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -61,36 +61,38 @@
 fun add_axms f args thy =
   f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
 
-val add_axioms = add_axms (#1 oo PureThy.add_axioms);
-val add_axioms_i = #1 oo PureThy.add_axioms_i;
+val add_axioms = add_axms (snd oo PureThy.add_axioms);
+val add_axioms_i = snd oo PureThy.add_axioms_i;
 fun add_defs (x, args) = add_axms (snd oo PureThy.add_defs x) args;
 fun add_defs_i (x, args) = (snd oo PureThy.add_defs_i x) args;
 
 
 (* theorems *)
 
-fun present_theorems kind (thy, named_thmss) =
+fun present_theorems kind (named_thmss, thy) =
   conditional (kind <> "" andalso kind <> Drule.internalK) (fn () =>
     Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);
 
 fun theorems kind args thy = thy
   |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
-  |> tap (present_theorems kind);
+  |> tap (present_theorems kind)
+  |> swap;
 
 fun theorems_i kind args =
   PureThy.note_thmss_i (Drule.kind kind) args
-  #> tap (present_theorems kind);
+  #> tap (present_theorems kind)
+  #> swap;
 
 fun apply_theorems args = apsnd (List.concat o map snd) o theorems "" [(("", []), args)];
 fun apply_theorems_i args = apsnd (List.concat o map snd) o theorems_i "" [(("", []), args)];
 
 fun smart_theorems kind NONE args thy = thy
       |> theorems kind args
-      |> tap (present_theorems kind)
+      |> tap (present_theorems kind o swap)
       |> (fn (thy, _) => (thy, ProofContext.init thy))
   | smart_theorems kind (SOME loc) args thy = thy
       |> Locale.note_thmss kind loc args
-      |> tap (present_theorems kind o apfst #1)
+      |> tap (present_theorems kind o swap o apfst #1)
       |> #1;
 
 fun declare_theorems opt_loc args =
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -1383,7 +1383,7 @@
   |> Theory.add_path (Sign.base_name name)
   |> Theory.no_base_names
   |> PureThy.note_thmss_i (Drule.kind kind) args
-  |>> Theory.restore_naming thy;
+  ||> Theory.restore_naming thy;
 
 
 (* accesses of interpreted theorems *)
@@ -1415,7 +1415,7 @@
   |> Theory.qualified_names
   |> Theory.custom_accesses (global_accesses prfx)
   |> PureThy.note_thmss_i kind args
-  |>> Theory.restore_naming thy;
+  ||> Theory.restore_naming thy;
 
 fun local_note_accesses_i prfx args ctxt =
   ctxt
@@ -1472,12 +1472,12 @@
               map (Attrib.global_attribute_i thy) (map inst_atts atts @ atts2)),
              [(map (Drule.standard o satisfy_protected prems o
             Element.inst_thm thy insts) ths, [])]));
-      in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
+      in global_note_accesses_i (Drule.kind kind) prfx args' thy |> snd end;
   in fold activate regs thy end;
 
 
-fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
-  | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
+fun smart_note_thmss kind NONE = swap oo PureThy.note_thmss_i (Drule.kind kind)
+  | smart_note_thmss kind (SOME loc) = swap oo note_thmss_qualified kind loc;
 
 
 local
@@ -1509,7 +1509,7 @@
       map (rpair [] o #1 o #1) args' ~~
       map (single o Thm.no_attributes o map export o #2) facts;
 
-    val (thy', result) =
+    val (result, thy') =
       thy
       |> put_facts loc args'
       |> note_thmss_registrations kind loc args'
@@ -1643,9 +1643,10 @@
           val elemss' = change_elemss axioms elemss @
             [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
         in
-          def_thy |> note_thmss_qualified "" aname
-            [((introN, []), [([intro], [])])]
-          |> #1 |> rpair (elemss', [statement])
+          def_thy
+          |> note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
+          |> snd
+          |> rpair (elemss', [statement])
         end;
     val (thy'', predicate) =
       if null ints then (thy', ([], []))
@@ -1655,10 +1656,12 @@
             thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
           val cstatement = Thm.cterm_of def_thy statement;
         in
-          def_thy |> note_thmss_qualified "" bname
-            [((introN, []), [([intro], [])]),
-             ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])]
-          |> #1 |> rpair ([cstatement], axioms)
+          def_thy
+          |> note_thmss_qualified "" bname
+               [((introN, []), [([intro], [])]),
+                ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])]
+          |> snd
+          |> rpair ([cstatement], axioms)
         end;
   in (thy'', (elemss', predicate)) end;
 
@@ -1707,7 +1710,7 @@
     val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))
   in
     pred_thy
-    |> note_thmss_qualified "" name facts' |> #1
+    |> note_thmss_qualified "" name facts' |> snd
     |> declare_locale name
     |> put_locale name {predicate = predicate, import = import,
         elems = map (fn e => (e, stamp ())) elems',
@@ -1883,7 +1886,7 @@
 fun global_activate_facts_elemss x = gen_activate_facts_elemss
       (fn thy => fn (name, ps) =>
         get_global_registration thy (name, map Logic.varify ps))
-      (global_note_accesses_i (Drule.kind ""))
+      (swap ooo global_note_accesses_i (Drule.kind ""))
       Attrib.global_attribute_i Drule.standard
       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
       (fn (n, ps) => fn (t, th) =>
@@ -2084,7 +2087,9 @@
                       |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
                       |> map (apfst (apfst (NameSpace.qualified prfx)))
                 in
-                  fst (global_note_accesses_i (Drule.kind "") prfx facts' thy)
+                  thy
+                  |> global_note_accesses_i (Drule.kind "") prfx facts'
+                  |> snd
                 end
               | activate_elem _ thy = thy;
 
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -622,7 +622,7 @@
 
 val local_results = gen_thmss ProofContext.note_thmss_i (K []) I I (K I);
 fun global_results kind =
-  swap oo (PureThy.note_thmss_i (Drule.kind kind) o map (apsnd Thm.simple_fact));
+  PureThy.note_thmss_i (Drule.kind kind) o map (apsnd Thm.simple_fact);
 
 fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
 fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/axclass.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -196,20 +196,20 @@
       (map inclass super_classes @ map (int_axm o #2) axms, inclass class);
 
     (*declare axioms and rule*)
-    val (axms_thy, ([intro], [axioms])) =
+    val (([intro], [axioms]), axms_thy) =
       class_thy
       |> Theory.add_path (Sign.const_of_class bclass)
       |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
-      |>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
+      ||>> 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 =
+    val (_, final_thy) =
       axms_thy
       |> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT --> propT)]
-      |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts))
-      |> Theory.restore_naming class_thy
-      |> AxclassesData.map (Symtab.update (class, info));
+      |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
+      ||> Theory.restore_naming class_thy
+      ||> AxclassesData.map (Symtab.update (class, info));
   in (final_thy, {intro = intro, axioms = axioms}) end;
 
 in
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/Pure/pure_thy.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -52,23 +52,23 @@
   val smart_store_thms_open: (bstring * thm list) -> thm list
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
-  val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
+  val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> thm list * theory
   val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
-    -> theory * thm list list
+    -> thm list list * theory 
   val note_thmss: theory attribute -> ((bstring * theory attribute list) *
     (thmref * theory attribute list) list) list ->
-    theory -> theory * (bstring * thm list) list
+    theory -> (bstring * thm list) list * theory
   val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
     (thm list * theory attribute list) list) list ->
-    theory -> theory * (bstring * thm list) list
+    theory -> (bstring * thm list) list * theory
   val add_axioms: ((bstring * string) * theory attribute list) list ->
-    theory -> theory * thm list
+    theory -> thm list * theory
   val add_axioms_i: ((bstring * term) * theory attribute list) list ->
-    theory -> theory * thm list
+    theory -> thm list * theory
   val add_axiomss: ((bstring * string list) * theory attribute list) list ->
-    theory -> theory * thm list list
+    theory -> thm list list * theory
   val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
-    theory -> theory * thm list list
+    theory -> thm list list * theory
   val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
     theory -> thm list * theory
   val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
@@ -340,14 +340,14 @@
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((bname, thms), atts) =
-  enter_thms pre_name (name_thms false)
+  swap o enter_thms pre_name (name_thms false)
     (Thm.applys_attributes o rpair atts) (bname, thms);
 
-fun gen_add_thmss pre_name args theory =
-  foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args);
+fun gen_add_thmss pre_name =
+  fold_map (add_thms_atts pre_name);
 
 fun gen_add_thms pre_name args =
-  apsnd (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
+  apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
 
 val add_thmss = gen_add_thmss (name_thms true);
 val add_thms = gen_add_thms (name_thms true);
@@ -370,8 +370,8 @@
 
 in
 
-val note_thmss = gen_note_thmss get_thms;
-val note_thmss_i = gen_note_thmss (K I);
+val note_thmss = swap ooo gen_note_thmss get_thms;
+val note_thmss_i = swap ooo gen_note_thmss (K I);
 
 end;
 
@@ -379,7 +379,7 @@
 (* store_thm *)
 
 fun store_thm ((bname, thm), atts) thy =
-  let val (thy', [th']) = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy
+  let val ([th'], thy') = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy
   in (th', thy') end;
 
 
@@ -430,32 +430,29 @@
 local
   fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name);
   fun get_axs thy named_axs = map (forall_elim_vars 0 o get_ax thy) named_axs;
-
-  fun add_single add (thy, ((name, ax), atts)) =
+  fun add_single add ((name, ax), atts) thy =
     let
       val named_ax = [(name, ax)];
       val thy' = add named_ax thy;
       val thm = hd (get_axs thy' named_ax);
-    in apsnd hd (gen_add_thms (K I) [((name, thm), atts)] thy') end;
-
-  fun add_multi add (thy, ((name, axs), atts)) =
+    in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end;
+  fun add_multi add ((name, axs), atts) thy =
     let
       val named_axs = name_multi name axs;
       val thy' = add named_axs thy;
       val thms = get_axs thy' named_axs;
-    in apsnd hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end;
-
-  fun add_singles add args thy = foldl_map (add_single add) (thy, args);
-  fun add_multis add args thy = foldl_map (add_multi add) (thy, args);
+    in apfst hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end;
+  fun add_singles add = fold_map (add_single add);
+  fun add_multis add = fold_map (add_multi add);
 in
   val add_axioms    = add_singles Theory.add_axioms;
   val add_axioms_i  = add_singles Theory.add_axioms_i;
   val add_axiomss   = add_multis Theory.add_axioms;
   val add_axiomss_i = add_multis Theory.add_axioms_i;
-  val add_defs      = swap ooo add_singles o Theory.add_defs;
-  val add_defs_i    = swap ooo add_singles o Theory.add_defs_i;
-  val add_defss     = swap ooo add_multis o Theory.add_defs;
-  val add_defss_i   = swap ooo add_multis o Theory.add_defs_i;
+  val add_defs      = add_singles o Theory.add_defs;
+  val add_defs_i    = add_singles o Theory.add_defs_i;
+  val add_defss     = add_multis o Theory.add_defs;
+  val add_defss_i   = add_multis o Theory.add_defs_i;
 end;
 
 
@@ -525,13 +522,13 @@
      Const ("TYPE", a_itselfT),
      Const (Term.dummy_patternN, aT)]
   |> Theory.add_modesyntax ("", false)
-    (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
+       (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Sign.local_path
-  |> (snd oo (add_defs_i false o map Thm.no_attributes))
-   [("prop_def", Logic.mk_equals (Logic.protect A, A))]
-  |> (#1 o add_thmss [(("nothing", []), [])])
+  |> (add_defs_i false o map Thm.no_attributes)
+       [("prop_def", Logic.mk_equals (Logic.protect A, A))] |> snd
+  |> add_thmss [(("nothing", []), [])] |> snd
   |> Theory.add_axioms_i Proofterm.equality_axms
   |> Theory.end_theory;
 
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -366,14 +366,14 @@
  in
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Theory.add_path big_rec_base_name
-        |> (#1 o PureThy.add_thmss
+        |> PureThy.add_thmss
          [(("simps", simps), [Simplifier.simp_add_global]),
           (("", intrs), [Classical.safe_intro_global]),
           (("con_defs", con_defs), []),
           (("case_eqns", case_eqns), []),
           (("recursor_eqns", recursor_eqns), []),
           (("free_iffs", free_iffs), []),
-          (("free_elims", free_SEs), [])])
+          (("free_elims", free_SEs), [])] |> snd
         |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
         |> ConstructorsData.map (fold Symtab.update con_pairs)
         |> Theory.parent_path,
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -165,7 +165,7 @@
   in
     thy
     |> Theory.add_path (Sign.base_name big_rec_name)
-    |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
+    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> snd
     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
     |> Theory.parent_path
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -175,8 +175,10 @@
           else ()
 
   (*add definitions of the inductive sets*)
-  val thy1 = thy |> Theory.add_path big_rec_base_name
-                 |> (snd o PureThy.add_defs_i false (map Thm.no_attributes axpairs))
+  val (_, thy1) =
+    thy
+    |> Theory.add_path big_rec_base_name
+    |> PureThy.add_defs_i false (map Thm.no_attributes axpairs)
 
 
   (*fetch fp definitions from the theory*)
@@ -510,9 +512,10 @@
                   |> standard
      and mutual_induct = CP.remove_split mutual_induct_fsplit
 
-     val (thy', [induct', mutual_induct']) = thy |> PureThy.add_thms
-      [((co_prefix ^ "induct", induct), [case_names, InductAttrib.induct_set_global big_rec_name]),
-       (("mutual_induct", mutual_induct), [case_names])];
+     val ([induct', mutual_induct'], thy') =
+       thy
+       |> PureThy.add_thms [((co_prefix ^ "induct", induct), [case_names, InductAttrib.induct_set_global big_rec_name]),
+            (("mutual_induct", mutual_induct), [case_names])];
     in ((thy', induct'), mutual_induct')
     end;  (*of induction_rules*)
 
@@ -520,23 +523,27 @@
 
   val ((thy2, induct), mutual_induct) =
     if not coind then induction_rules raw_induct thy1
-    else (thy1 |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])] |> apsnd hd, TrueI)
+    else
+      (thy1
+      |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])]
+      |> apfst hd |> Library.swap, TrueI)
   and defs = big_rec_def :: part_rec_defs
 
 
-  val (thy3, ([bnd_mono', dom_subset', elim'], [defs', intrs'])) =
+  val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) =
     thy2
     |> IndCases.declare big_rec_name make_cases
     |> PureThy.add_thms
       [(("bnd_mono", bnd_mono), []),
        (("dom_subset", dom_subset), []),
        (("cases", elim), [case_names, InductAttrib.cases_set_global big_rec_name])]
-    |>>> (PureThy.add_thmss o map Thm.no_attributes)
+    ||>> (PureThy.add_thmss o map Thm.no_attributes)
         [("defs", defs),
          ("intros", intrs)];
-  val (thy4, intrs'') =
-    thy3 |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
-    |>> Theory.parent_path;
+  val (intrs'', thy4) =
+    thy3
+    |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
+    ||> Theory.parent_path;
   in
     (thy4,
       {defs = defs',
diff -r 2ef0183fa20b -r 0e1d025d57b3 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -186,10 +186,13 @@
         standard (Goal.prove thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
           (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))));
 
-    val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
-    val thy3 = thy2
-      |> (#1 o PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])])
-      |> Theory.parent_path;
+    val (eqn_thms', thy2) =
+      thy1
+      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
+    val (_, thy3) =
+      thy2
+      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])]
+      ||> Theory.parent_path;
   in (thy3, eqn_thms') end;
 
 fun add_primrec args thy =