re-arranged tuples (theory * 'a) to ('a * theory) in Pure

--- a/src/HOL/Tools/datatype_package.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -766,13 +766,11 @@
   let
     val _ = Theory.requires thy0 "Inductive" "datatype representations";
 
-    fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs);
-    fun app_thm src thy = apsnd hd (apply_theorems [src] thy);
-
-    val (((thy1, induction), inject), distinct) = thy0
-      |> app_thmss raw_distinct
-      |> apfst (app_thmss raw_inject)
-      |> apfst (apfst (app_thm raw_induction));
+    val (((distinct, inject), [induction]), thy1) =
+      thy0
+      |> fold_map apply_theorems raw_distinct
+      ||>> fold_map apply_theorems raw_inject
+      ||>> apply_theorems [raw_induction];
     val sign = Theory.sign_of thy1;
 
     val induction' = freezeT induction;

--- a/src/HOL/Tools/inductive_package.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -583,7 +583,7 @@
 
     val facts = args |> map (fn ((a, atts), props) =>
      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
-  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
+  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
@@ -864,7 +864,7 @@
     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
     val (cs', intr_ts') = unify_consts thy cs intr_ts;
 
-    val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
+    val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
   in
     add_inductive_i verbose false "" coind false false cs'
       ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'

--- a/src/HOL/Tools/recdef_package.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -272,7 +272,7 @@
     val _ = requires_recdef thy;
     val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
 
-    val (thy1, congs) = thy |> app_thms raw_congs;
+    val (congs, thy1) = thy |> app_thms raw_congs;
     val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
     val ([induct_rules'], thy3) =
       thy2

--- a/src/HOL/Tools/specification_package.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -191,7 +191,6 @@
                         fun undo_imps thm =
                             equal_elim (symmetric rew_imp) thm
 
-                        fun apply_atts arg = Thm.apply_attributes (arg, map (Attrib.global_attribute thy) atts)
                         fun add_final (arg as (thy, thm)) =
                             if name = ""
                             then arg |> Library.swap
@@ -201,7 +200,7 @@
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
                              |> apsnd standard
-                             |> apply_atts
+                             |> Thm.apply_attributes (map (Attrib.global_attribute thy) atts)
                              |> add_final
                              |> Library.swap
                     end

--- a/src/Pure/Isar/attrib.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -180,7 +180,7 @@
     let
       val ths = PureThy.select_thm thmref fact;
       val atts = map (attrib (theory_of st)) srcs;
-      val (st', ths') = Thm.applys_attributes ((st, ths), atts);
+      val (st', ths') = Thm.applys_attributes atts (st, ths);
     in (st', pick name ths') end));
 
 val global_thm = gen_thm I global_attribute_i PureThy.get_thms PureThy.single_thm;

--- a/src/Pure/Isar/context_rules.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/Isar/context_rules.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -258,7 +258,7 @@
 (* low-level modifiers *)
 
 fun modifier att (x, ths) =
-  #1 (Thm.applys_attributes ((x, rev ths), [att]));
+  fst (Thm.applys_attributes [att] (x, rev ths));
 
 val addXIs_global = modifier (intro_query_global NONE);
 val addXEs_global = modifier (elim_query_global NONE);

--- a/src/Pure/Isar/isar_thy.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -11,14 +11,14 @@
   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
   val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
-  val apply_theorems: (thmref * Attrib.src list) list -> theory -> theory * thm list
-  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
+  val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
+  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> thm list * theory
   val theorems: string ->
     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
-    -> theory -> theory * (string * thm list) list
+    -> theory -> (string * thm list) list * theory 
   val theorems_i: string ->
     ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
-    -> theory -> theory * (string * thm list) list
+    -> theory -> (string * thm list) list * theory
   val smart_theorems: string -> xstring option ->
     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
     theory -> theory * Proof.context
@@ -75,21 +75,19 @@
 
 fun theorems kind args thy = thy
   |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
-  |> tap (present_theorems kind)
-  |> swap;
+  |> tap (present_theorems kind);
 
 fun theorems_i kind args =
   PureThy.note_thmss_i (Drule.kind kind) args
-  #> tap (present_theorems kind)
-  #> swap;
+  #> tap (present_theorems kind);
 
-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 apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)];
+fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)];
 
 fun smart_theorems kind NONE args thy = thy
       |> theorems kind args
-      |> tap (present_theorems kind o swap)
-      |> (fn (thy, _) => (thy, ProofContext.init thy))
+      |> tap (present_theorems kind)
+      |> (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 swap o apfst #1)

--- a/src/Pure/Isar/method.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/Isar/method.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -624,7 +624,7 @@
 fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
 fun thmss ss = Scan.repeat (thms ss) >> List.concat;
 
-fun apply (f, att) (ctxt, ths) = Thm.applys_attributes ((f ctxt, ths), [att]);
+fun apply (f, att) (ctxt, ths) = Thm.applys_attributes [att] (f ctxt, ths);
 
 fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
   Scan.succeed (apply m (ctxt, ths)))) >> #2;

--- a/src/Pure/Isar/proof_context.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -1018,7 +1018,7 @@
 fun gen_note_thmss get = fold_map (fn ((name, more_attrs), ths_attrs) => fn ctxt =>
   let
     fun app (th, attrs) (ct, ths) =
-      let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
+      let val (ct', th') = Thm.applys_attributes (attrs @ more_attrs) (ct, get ctxt th)
       in (ct', th' :: ths) end;
     val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []);
     val thms = List.concat (rev rev_thms);

--- a/src/Pure/axclass.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/axclass.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -11,9 +11,9 @@
   val print_axclasses: theory -> unit
   val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
   val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
-    theory -> theory * {intro: thm, axioms: thm list}
+    theory -> {intro: thm, axioms: thm list} * theory
   val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
-    theory -> theory * {intro: thm, axioms: thm list}
+    theory -> {intro: thm, axioms: thm list} * theory
   val add_classrel_thms: thm list -> theory -> theory
   val add_arity_thms: thm list -> theory -> theory
   val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
@@ -210,7 +210,7 @@
       |> 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 ({intro = intro, axioms = axioms}, final_thy) end;
 
 in
 
@@ -347,7 +347,7 @@
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
         P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name
-      >> (Toplevel.theory o (#1 oo uncurry add_axclass)));
+      >> (Toplevel.theory o (snd oo uncurry add_axclass)));
 
 val instanceP =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal

--- a/src/Pure/pure_thy.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/pure_thy.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -308,8 +308,8 @@
 fun name_thmss name xs =
   (case filter_out (null o fst) xs of
     [([x], z)] => [([name_thm true (name, x)], z)]
-  | _ => snd (foldl_map (fn (i, (ys, z)) =>
-    (i + length ys, (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
+  | _ => fst (fold_map (fn (ys, z) => fn i =>
+    ((map (name_thm true) (gen_names i (length ys) name ~~ ys), z), i + length ys)) xs 0));
 
 
 (* enter_thms *)
@@ -317,7 +317,7 @@
 fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
 fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
 
-fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms)
+fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap
   | enter_thms pre_name post_name app_att (bname, thms) thy =
       let
         val name = Sign.full_name thy bname;
@@ -333,15 +333,15 @@
             if Thm.eq_thms (thms', thms'') then warn_same name
             else warn_overwrite name);
         r := {theorems = (space', theorems'), index = index'};
-        (thy', thms')
+        (thms', thy')
       end;
 
 
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((bname, thms), atts) =
-  swap o enter_thms pre_name (name_thms false)
-    (Thm.applys_attributes o rpair atts) (bname, thms);
+  enter_thms pre_name (name_thms false)
+    (Thm.applys_attributes atts) (bname, thms);
 
 fun gen_add_thmss pre_name =
   fold_map (add_thms_atts pre_name);
@@ -357,21 +357,21 @@
 
 local
 
-fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
+fun gen_note_thss get kind_att ((bname, more_atts), ths_atts) thy =
   let
-    fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
-    val (thy', thms) = thy |> enter_thms
+    fun app (x, (ths, atts)) = Thm.applys_attributes atts (x, ths);
+    val (thms, thy') = thy |> enter_thms
       name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
       (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
-  in (thy', (bname, thms)) end;
+  in ((bname, thms), thy') end;
 
-fun gen_note_thmss get kind_att args thy =
-  foldl_map (gen_note_thss get kind_att) (thy, args);
+fun gen_note_thmss get kind_att =
+  fold_map (gen_note_thss get kind_att);
 
 in
 
-val note_thmss = swap ooo gen_note_thmss get_thms;
-val note_thmss_i = swap ooo gen_note_thmss (K I);
+val note_thmss = gen_note_thmss get_thms;
+val note_thmss_i = gen_note_thmss (K I);
 
 end;
 
@@ -390,12 +390,12 @@
 fun smart_store _ (name, []) =
       error ("Cannot store empty list of theorems: " ^ quote name)
   | smart_store name_thm (name, [thm]) =
-      #2 (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
+      fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
   | smart_store name_thm (name, thms) =
       let
         fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
         val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
-      in #2 (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
+      in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
 
 in
 

--- a/src/Pure/thm.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/Pure/thm.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -142,8 +142,8 @@
   val no_prems: thm -> bool
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
-  val apply_attributes: ('a * thm) * 'a attribute list -> 'a * thm
-  val applys_attributes: ('a * thm list) * 'a attribute list -> 'a * thm list
+  val apply_attributes: 'a attribute list -> 'a * thm -> 'a * thm
+  val applys_attributes: 'a attribute list -> 'a * thm list -> 'a * thm list
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val get_name_tags: thm -> string * tag list
@@ -400,8 +400,8 @@
 
 fun no_attributes x = (x, []);
 fun simple_fact x = [(x, [])];
-fun apply_attributes (x_th, atts) = Library.apply atts x_th;
-fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
+val apply_attributes = Library.apply;
+fun applys_attributes atts = foldl_map (Library.apply atts);
 
 
 (* hyps *)

--- a/src/ZF/Tools/datatype_package.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -394,13 +394,14 @@
     val dom_sum =
       if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
       else read_i sdom;
-
-    val (thy', ((monos, type_intrs), type_elims)) = thy
-      |> IsarThy.apply_theorems raw_monos
-      |>>> IsarThy.apply_theorems raw_type_intrs
-      |>>> IsarThy.apply_theorems raw_type_elims;
-  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy' end;
-
+  in
+    thy
+    |> IsarThy.apply_theorems raw_monos
+    ||>> IsarThy.apply_theorems raw_type_intrs
+    ||>> IsarThy.apply_theorems raw_type_elims
+    |-> (fn ((monos, type_intrs), type_elims) =>
+          add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims))
+  end;
 
 (* outer syntax *)
 

--- a/src/ZF/Tools/ind_cases.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -55,7 +55,7 @@
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.global_attribute thy) srcs),
         map (Thm.no_attributes o single o mk_cases) props));
-  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
+  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
 
 
 (* ind_cases method *)

--- a/src/ZF/Tools/induct_tacs.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -172,16 +172,14 @@
   end;
 
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
-  let
-    val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy
-      |> IsarThy.apply_theorems [raw_elim]
-      |>>> IsarThy.apply_theorems [raw_induct]
-      |>>> IsarThy.apply_theorems raw_case_eqns
-      |>>> IsarThy.apply_theorems raw_recursor_eqns;
-  in
-    thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims)
-      (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns
-  end;
+  thy
+  |> IsarThy.apply_theorems [raw_elim]
+  ||>> IsarThy.apply_theorems [raw_induct]
+  ||>> IsarThy.apply_theorems raw_case_eqns
+  ||>> IsarThy.apply_theorems raw_recursor_eqns
+  |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
+          rep_datatype_i (PureThy.single_thm "elimination" elims)
+            (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
 
 
 (* theory setup *)

--- a/src/ZF/Tools/inductive_package.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -567,16 +567,16 @@
     val dom_sum = read Ind_Syntax.iT sdom_sum;
     val intr_tms = map (read propT o snd o fst) sintrs;
     val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
-
-    val (thy', (((monos, con_defs), type_intrs), type_elims)) = thy
-      |> IsarThy.apply_theorems raw_monos
-      |>>> IsarThy.apply_theorems raw_con_defs
-      |>>> IsarThy.apply_theorems raw_type_intrs
-      |>>> IsarThy.apply_theorems raw_type_elims;
   in
-    add_inductive_i true (rec_tms, dom_sum) intr_specs
-      (monos, con_defs, type_intrs, type_elims) thy'
-  end
+    thy
+    |> IsarThy.apply_theorems raw_monos
+    ||>> IsarThy.apply_theorems raw_con_defs
+    ||>> IsarThy.apply_theorems raw_type_intrs
+    ||>> IsarThy.apply_theorems raw_type_elims
+    |-> (fn (((monos, con_defs), type_intrs), type_elims) =>
+          add_inductive_i true (rec_tms, dom_sum) intr_specs
+            (monos, con_defs, type_intrs, type_elims))
+  end;
 
 
 (* outer syntax *)