oriented result pairs in PureThy
authorhaftmann
Fri Dec 09 09:06:45 2005 +0100 (2005-12-09)
changeset 183770e1d025d57b3
parent 18376 2ef0183fa20b
child 18378 35fba71ec6ef
oriented result pairs in PureThy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/fixrec_package.ML
src/HOLCF/pcpodef_package.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/axclass.ML
src/Pure/pure_thy.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Dec 08 20:16:17 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Dec 09 09:06:45 2005 +0100
     1.3 @@ -262,7 +262,7 @@
     1.4    in
     1.5      thy2
     1.6      |> Theory.add_path (space_implode "_" new_type_names)
     1.7 -    |> PureThy.add_thmss [(("recs", rec_thms), [])] |> Library.swap
     1.8 +    |> PureThy.add_thmss [(("recs", rec_thms), [])]
     1.9      ||> Theory.parent_path
    1.10      |-> (fn thms => pair (reccomb_names, Library.flat thms))
    1.11    end;
    1.12 @@ -439,7 +439,7 @@
    1.13    in
    1.14      thy'
    1.15      |> Theory.add_path big_name
    1.16 -    |> PureThy.add_thmss [(("size", size_thms), [])] |> Library.swap
    1.17 +    |> PureThy.add_thmss [(("size", size_thms), [])]
    1.18      ||> Theory.parent_path
    1.19      |-> (fn thmss => pair (Library.flat thmss))
    1.20    end;
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Dec 08 20:16:17 2005 +0100
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Dec 09 09:06:45 2005 +0100
     2.3 @@ -81,21 +81,21 @@
     2.4  
     2.5  (* store theorems in theory *)
     2.6  
     2.7 -fun store_thmss_atts label tnames attss thmss thy =
     2.8 -  (thy, tnames ~~ attss ~~ thmss) |>
     2.9 -  foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
    2.10 -    Theory.add_path tname |>
    2.11 -    (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
    2.12 -    Theory.parent_path) |> Library.swap;
    2.13 +fun store_thmss_atts label tnames attss thmss =
    2.14 +  fold_map (fn ((tname, atts), thms) =>
    2.15 +    Theory.add_path tname
    2.16 +    #> PureThy.add_thmss [((label, thms), atts)]
    2.17 +    #-> (fn thm::_ => Theory.parent_path #> pair thm)
    2.18 +  ) (tnames ~~ attss ~~ thmss);
    2.19  
    2.20  fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
    2.21  
    2.22 -fun store_thms_atts label tnames attss thms thy =
    2.23 -  (thy, tnames ~~ attss ~~ thms) |>
    2.24 -  foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
    2.25 -    Theory.add_path tname |>
    2.26 -    (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
    2.27 -    Theory.parent_path) |> Library.swap;
    2.28 +fun store_thms_atts label tnames attss thmss =
    2.29 +  fold_map (fn ((tname, atts), thms) =>
    2.30 +    Theory.add_path tname
    2.31 +    #> PureThy.add_thms [((label, thms), atts)]
    2.32 +    #-> (fn thm::_ => Theory.parent_path #> pair thm)
    2.33 +  ) (tnames ~~ attss ~~ thmss);
    2.34  
    2.35  fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
    2.36  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 08 20:16:17 2005 +0100
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Dec 09 09:06:45 2005 +0100
     3.3 @@ -286,7 +286,7 @@
     3.4        
     3.5  fun add_rules simps case_thms size_thms rec_thms inject distinct
     3.6                    weak_case_congs cong_att =
     3.7 -  (#1 o PureThy.add_thmss [(("simps", simps), []),
     3.8 +  (snd o PureThy.add_thmss [(("simps", simps), []),
     3.9      (("", List.concat case_thms @ size_thms @ 
    3.10            List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
    3.11      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
    3.12 @@ -313,7 +313,7 @@
    3.13      fun unnamed_rule i =
    3.14        (("", proj i induction), [InductAttrib.induct_type_global ""]);
    3.15      val rules = List.concat (map named_rules infos) @ map unnamed_rule (length infos upto n - 1);
    3.16 -  in #1 o PureThy.add_thms rules end;
    3.17 +  in snd o PureThy.add_thms rules end;
    3.18  
    3.19  
    3.20  
    3.21 @@ -533,11 +533,12 @@
    3.22  fun add_and_get_axioms_atts label tnames attss ts thy =
    3.23    foldr (fn (((tname, atts), t), (thy', axs)) =>
    3.24      let
    3.25 -      val (thy'', [ax]) = thy' |>
    3.26 -        Theory.add_path tname |>
    3.27 -        PureThy.add_axioms_i [((label, t), atts)];
    3.28 +      val ([ax], thy'') =
    3.29 +        thy'
    3.30 +        |> Theory.add_path tname
    3.31 +        |> PureThy.add_axioms_i [((label, t), atts)];
    3.32      in (Theory.parent_path thy'', ax::axs)
    3.33 -    end) (thy, []) (tnames ~~ attss ~~ ts);
    3.34 +    end) (thy, []) (tnames ~~ attss ~~ ts) |> swap;
    3.35  
    3.36  fun add_and_get_axioms label tnames =
    3.37    add_and_get_axioms_atts label tnames (replicate (length tnames) []);
    3.38 @@ -545,11 +546,12 @@
    3.39  fun add_and_get_axiomss label tnames tss thy =
    3.40    foldr (fn ((tname, ts), (thy', axss)) =>
    3.41      let
    3.42 -      val (thy'', [axs]) = thy' |>
    3.43 -        Theory.add_path tname |>
    3.44 -        PureThy.add_axiomss_i [((label, ts), [])];
    3.45 +      val ([axs], thy'') =
    3.46 +        thy'
    3.47 +        |> Theory.add_path tname
    3.48 +        |> PureThy.add_axiomss_i [((label, ts), [])];
    3.49      in (Theory.parent_path thy'', axs::axss)
    3.50 -    end) (thy, []) (tnames ~~ tss);
    3.51 +    end) (thy, []) (tnames ~~ tss) |> swap;
    3.52  
    3.53  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    3.54      case_names_induct case_names_exhausts thy =
    3.55 @@ -639,35 +641,35 @@
    3.56      val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
    3.57      val size_axs = if no_size then [] else DatatypeProp.make_size descr sorts thy2;
    3.58  
    3.59 -    val (thy3, (([induct], [rec_thms]), inject)) =
    3.60 -      thy2 |>
    3.61 -      Theory.add_path (space_implode "_" new_type_names) |>
    3.62 -      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
    3.63 -        [case_names_induct])] |>>>
    3.64 -      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
    3.65 -      (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
    3.66 -      Theory.parent_path |>>>
    3.67 -      add_and_get_axiomss "inject" new_type_names
    3.68 -        (DatatypeProp.make_injs descr sorts);
    3.69 +    val ((([induct], [rec_thms]), inject), thy3) =
    3.70 +      thy2
    3.71 +      |> Theory.add_path (space_implode "_" new_type_names)
    3.72 +      |> PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
    3.73 +          [case_names_induct])]
    3.74 +      ||>> PureThy.add_axiomss_i [(("recs", rec_axs), [])]
    3.75 +      ||> (if no_size then I else snd o PureThy.add_axiomss_i [(("size", size_axs), [])])
    3.76 +      ||> Theory.parent_path
    3.77 +      ||>> add_and_get_axiomss "inject" new_type_names
    3.78 +            (DatatypeProp.make_injs descr sorts);
    3.79      val size_thms = if no_size then [] else get_thms thy3 (Name "size");
    3.80 -    val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
    3.81 +    val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
    3.82        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
    3.83  
    3.84      val exhaust_ts = DatatypeProp.make_casedists descr sorts;
    3.85 -    val (thy5, exhaustion) = add_and_get_axioms_atts "exhaust" new_type_names
    3.86 +    val (exhaustion, thy5) = add_and_get_axioms_atts "exhaust" new_type_names
    3.87        (map Library.single case_names_exhausts) exhaust_ts thy4;
    3.88 -    val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
    3.89 +    val (case_thms, thy6) = add_and_get_axiomss "cases" new_type_names
    3.90        (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
    3.91      val (split_ts, split_asm_ts) = ListPair.unzip
    3.92        (DatatypeProp.make_splits new_type_names descr sorts thy6);
    3.93 -    val (thy7, split) = add_and_get_axioms "split" new_type_names split_ts thy6;
    3.94 -    val (thy8, split_asm) = add_and_get_axioms "split_asm" new_type_names
    3.95 +    val (split, thy7) = add_and_get_axioms "split" new_type_names split_ts thy6;
    3.96 +    val (split_asm, thy8) = add_and_get_axioms "split_asm" new_type_names
    3.97        split_asm_ts thy7;
    3.98 -    val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
    3.99 +    val (nchotomys, thy9) = add_and_get_axioms "nchotomy" new_type_names
   3.100        (DatatypeProp.make_nchotomys descr sorts) thy8;
   3.101 -    val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
   3.102 +    val (case_congs, thy10) = add_and_get_axioms "case_cong" new_type_names
   3.103        (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
   3.104 -    val (thy11, weak_case_congs) = add_and_get_axioms "weak_case_cong" new_type_names
   3.105 +    val (weak_case_congs, thy11) = add_and_get_axioms "weak_case_cong" new_type_names
   3.106        (DatatypeProp.make_weak_case_congs new_type_names descr sorts thy10) thy10;
   3.107  
   3.108      val dt_infos = map (make_dt_info descr' sorts induct reccomb_names' rec_thms)
   3.109 @@ -831,11 +833,12 @@
   3.110            [descr] sorts reccomb_names rec_thms thy8
   3.111        else ([], thy8);
   3.112  
   3.113 -    val ([induction'], thy10) = thy9 |>
   3.114 -      store_thmss "inject" new_type_names inject |> snd |>
   3.115 -      store_thmss "distinct" new_type_names distinct |> snd |>
   3.116 -      Theory.add_path (space_implode "_" new_type_names) |>
   3.117 -      PureThy.add_thms [(("induct", induction), [case_names_induct])] |> Library.swap;
   3.118 +    val ((_, [induction']), thy10) =
   3.119 +      thy9
   3.120 +      |> store_thmss "inject" new_type_names inject
   3.121 +      ||>> store_thmss "distinct" new_type_names distinct
   3.122 +      ||> Theory.add_path (space_implode "_" new_type_names)
   3.123 +      ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
   3.124  
   3.125      val dt_infos = map (make_dt_info descr sorts induction' reccomb_names rec_thms)
   3.126        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 08 20:16:17 2005 +0100
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Dec 09 09:06:45 2005 +0100
     4.3 @@ -226,9 +226,10 @@
     4.4          val def_name = (Sign.base_name cname) ^ "_def";
     4.5          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
     4.6            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
     4.7 -        val ([def_thm], thy') = thy |>
     4.8 -          Theory.add_consts_i [(cname', constrT, mx)] |>
     4.9 -          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
    4.10 +        val ([def_thm], thy') =
    4.11 +          thy
    4.12 +          |> Theory.add_consts_i [(cname', constrT, mx)]
    4.13 +          |> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
    4.14  
    4.15        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    4.16  
    4.17 @@ -639,10 +640,11 @@
    4.18              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
    4.19                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]));
    4.20  
    4.21 -    val (thy7, [dt_induct']) = thy6 |>
    4.22 -      Theory.add_path big_name |>
    4.23 -      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    4.24 -      Theory.parent_path;
    4.25 +    val ([dt_induct'], thy7) =
    4.26 +      thy6
    4.27 +      |> Theory.add_path big_name
    4.28 +      |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
    4.29 +      ||> Theory.parent_path;
    4.30  
    4.31    in
    4.32      ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
     5.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 08 20:16:17 2005 +0100
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 09 09:06:45 2005 +0100
     5.3 @@ -451,13 +451,13 @@
     5.4      fun cases_spec name elim thy =
     5.5        thy
     5.6        |> Theory.add_path (Sign.base_name name)
     5.7 -      |> (fst o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
     5.8 +      |> (snd o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
     5.9        |> Theory.parent_path;
    5.10      val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    5.11  
    5.12      val induct_att =
    5.13        if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
    5.14 -    fun induct_spec (name, th) = #1 o PureThy.add_thms
    5.15 +    fun induct_spec (name, th) = snd o PureThy.add_thms
    5.16        [(("", RuleCases.save induct th), [induct_att name])];
    5.17      val induct_specs =
    5.18        if no_induct then [] else map induct_spec (project_rules names induct);
    5.19 @@ -794,16 +794,17 @@
    5.20          (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
    5.21        else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
    5.22  
    5.23 -    val (thy2, intrs') =
    5.24 -      thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
    5.25 -    val (thy3, ([_, elims'], [induct'])) =
    5.26 +    val (intrs', thy2) =
    5.27 +      thy1
    5.28 +      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
    5.29 +    val (([_, elims'], [induct']), thy3) =
    5.30        thy2
    5.31        |> PureThy.add_thmss
    5.32          [(("intros", intrs'), []),
    5.33            (("elims", elims), [RuleCases.consumes 1])]
    5.34 -      |>>> PureThy.add_thms
    5.35 +      ||>> PureThy.add_thms
    5.36          [((coind_prefix coind ^ "induct", rulify (#1 induct)), #2 induct)]
    5.37 -      |>> Theory.parent_path;
    5.38 +      ||> Theory.parent_path;
    5.39    in (thy3,
    5.40      {defs = fp_def :: rec_sets_defs,
    5.41       mono = mono,
     6.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Dec 08 20:16:17 2005 +0100
     6.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Dec 09 09:06:45 2005 +0100
     6.3 @@ -255,11 +255,11 @@
     6.4        commas_quote (map fst nameTs1) ^ " ...");
     6.5      val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t
     6.6          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
     6.7 -    val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     6.8 +    val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     6.9      val thy''' = thy''
    6.10 -      |> (#1 o PureThy.add_thmss [(("simps", simps'),
    6.11 +      |> (snd o PureThy.add_thmss [(("simps", simps'),
    6.12             [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
    6.13 -      |> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
    6.14 +      |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
    6.15        |> Theory.parent_path
    6.16    in
    6.17      (thy''', simps')
     7.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Dec 08 20:16:17 2005 +0100
     7.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Dec 09 09:06:45 2005 +0100
     7.3 @@ -245,11 +245,11 @@
     7.4      val simp_att = if null tcs then
     7.5        [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
     7.6  
     7.7 -    val (thy, (simps' :: rules', [induct'])) =
     7.8 +    val ((simps' :: rules', [induct']), thy) =
     7.9        thy
    7.10        |> Theory.add_path bname
    7.11        |> PureThy.add_thmss ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    7.12 -      |>>> PureThy.add_thms [(("induct", induct), [])];
    7.13 +      ||>> PureThy.add_thms [(("induct", induct), [])];
    7.14      val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
    7.15      val thy =
    7.16        thy
    7.17 @@ -274,11 +274,11 @@
    7.18  
    7.19      val (thy1, congs) = thy |> app_thms raw_congs;
    7.20      val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
    7.21 -    val (thy3, [induct_rules']) =
    7.22 +    val ([induct_rules'], thy3) =
    7.23        thy2
    7.24        |> Theory.add_path bname
    7.25        |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
    7.26 -      |>> Theory.parent_path;
    7.27 +      ||> Theory.parent_path;
    7.28    in (thy3, {induct_rules = induct_rules'}) end;
    7.29  
    7.30  val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
     8.1 --- a/src/HOL/Tools/record_package.ML	Thu Dec 08 20:16:17 2005 +0100
     8.2 +++ b/src/HOL/Tools/record_package.ML	Fri Dec 09 09:06:45 2005 +0100
     8.3 @@ -1282,7 +1282,7 @@
     8.4               (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV NONE
     8.5               (Tactic.rtac UNIV_witness 1))
     8.6      val rewrite_rule = Tactic.rewrite_rule [def, rec_UNIV_I, rec_True_simp];
     8.7 -  in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct])
     8.8 +  in (map rewrite_rule [abs_inject, abs_inverse, abs_induct], thy')
     8.9    end;
    8.10  
    8.11  fun mixit convs refls =
    8.12 @@ -1348,10 +1348,11 @@
    8.13      fun mk_defs () =
    8.14        thy
    8.15          |> extension_typedef name repT (alphas@[zeta])
    8.16 -        |>> Theory.add_consts_i
    8.17 +        ||> Theory.add_consts_i
    8.18                (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
    8.19 -        |>>> (PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs)) #> Library.swap)
    8.20 -        |>>> (PureThy.add_defs_i false (map Thm.no_attributes upd_specs) #> Library.swap)
    8.21 +        ||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
    8.22 +        ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
    8.23 +        |> swap
    8.24      val (defs_thy, (([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs),upd_defs)) =
    8.25          timeit_msg "record extension type/selector/update defs:" mk_defs;
    8.26  
    8.27 @@ -1500,8 +1501,8 @@
    8.28                  REPEAT (etac meta_allE 1), atac 1]);
    8.29      val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
    8.30  
    8.31 -    val (thm_thy,([inject',induct',cases',surjective',split_meta'],
    8.32 -                  [dest_convs',upd_convs'])) =
    8.33 +    val (([inject',induct',cases',surjective',split_meta'], [dest_convs',upd_convs']),
    8.34 +      thm_thy) =
    8.35        defs_thy
    8.36        |> (PureThy.add_thms o map Thm.no_attributes)
    8.37             [("ext_inject", inject),
    8.38 @@ -1509,7 +1510,7 @@
    8.39              ("ext_cases", cases),
    8.40              ("ext_surjective", surjective),
    8.41              ("ext_split", split_meta)]
    8.42 -      |>>> (PureThy.add_thmss o map Thm.no_attributes)
    8.43 +      ||>> (PureThy.add_thmss o map Thm.no_attributes)
    8.44                [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)]
    8.45  
    8.46    in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs')
    8.47 @@ -1740,7 +1741,6 @@
    8.48              ([],[],field_tr's, [])
    8.49          |> Theory.add_advanced_trfuns
    8.50              ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
    8.51 -
    8.52          |> Theory.parent_path
    8.53          |> Theory.add_tyabbrs_i recordT_specs
    8.54          |> Theory.add_path bname
    8.55 @@ -1748,10 +1748,11 @@
    8.56              (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
    8.57          |> (Theory.add_consts_i o map Syntax.no_syn)
    8.58              (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
    8.59 -        |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs #> Library.swap)
    8.60 -        |>>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs #> Library.swap)
    8.61 -        |>>> ((PureThy.add_defs_i false o map Thm.no_attributes)
    8.62 -               [make_spec, fields_spec, extend_spec, truncate_spec] #> Library.swap)
    8.63 +        |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
    8.64 +        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
    8.65 +        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
    8.66 +               [make_spec, fields_spec, extend_spec, truncate_spec])
    8.67 +        |> swap
    8.68      val (defs_thy,((sel_defs,upd_defs),derived_defs)) =
    8.69          timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
    8.70           mk_defs;
    8.71 @@ -1967,9 +1968,8 @@
    8.72        end);
    8.73       val equality = timeit_msg "record equality proof:" equality_prf;
    8.74  
    8.75 -    val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
    8.76 -                    derived_defs'],
    8.77 -                   [surjective',equality']),[induct_scheme',induct',cases_scheme',cases'])) =
    8.78 +    val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'],
    8.79 +            [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) =
    8.80        defs_thy
    8.81        |> (PureThy.add_thmss o map Thm.no_attributes)
    8.82           [("select_convs", sel_convs_standard),
    8.83 @@ -1978,10 +1978,10 @@
    8.84            ("update_defs", upd_defs),
    8.85            ("splits", [split_meta_standard,split_object,split_ex]),
    8.86            ("defs", derived_defs)]
    8.87 -      |>>> (PureThy.add_thms o map Thm.no_attributes)
    8.88 +      ||>> (PureThy.add_thms o map Thm.no_attributes)
    8.89            [("surjective", surjective),
    8.90             ("equality", equality)]
    8.91 -      |>>> PureThy.add_thms
    8.92 +      ||>> PureThy.add_thms
    8.93          [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
    8.94           (("induct", induct), induct_type_global name),
    8.95           (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
    8.96 @@ -1992,7 +1992,7 @@
    8.97      val iffs = [ext_inject]
    8.98      val final_thy =
    8.99        thms_thy
   8.100 -      |> (#1 oo PureThy.add_thmss)
   8.101 +      |> (snd oo PureThy.add_thmss)
   8.102            [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
   8.103             (("iffs",iffs), [iff_add_global])]
   8.104        |> put_record name (make_record_info args parent fields extension induct_scheme')
     9.1 --- a/src/HOL/Tools/specification_package.ML	Thu Dec 08 20:16:17 2005 +0100
     9.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Dec 09 09:06:45 2005 +0100
     9.3 @@ -49,7 +49,7 @@
     9.4          let
     9.5              fun process [] (thy,tm) =
     9.6                  let
     9.7 -                    val (thy',thms) = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
     9.8 +                    val (thms, thy') = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
     9.9                  in
    9.10                      (thy',hd thms)
    9.11                  end
    10.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Dec 08 20:16:17 2005 +0100
    10.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Dec 09 09:06:45 2005 +0100
    10.3 @@ -159,14 +159,14 @@
    10.4          [(Rep_name, newT --> oldT, NoSyn),
    10.5           (Abs_name, oldT --> newT, NoSyn)])
    10.6        |> add_def def (Logic.mk_defpair (setC, set))
    10.7 -      ||>> (PureThy.add_axioms_i [((typedef_name, typedef_prop),
    10.8 -          [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] #> Library.swap)
    10.9 +      ||>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
   10.10 +          [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
   10.11        ||> Theory.add_finals_i false [RepC, AbsC]
   10.12        |-> (fn (set_def, [type_definition]) => fn theory' =>
   10.13          let
   10.14            fun make th = Drule.standard (th OF [type_definition]);
   10.15 -          val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   10.16 -              Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
   10.17 +          val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   10.18 +              Rep_cases, Abs_cases, Rep_induct, Abs_induct], theory'') =
   10.19              theory'
   10.20              |> Theory.add_path name
   10.21              |> PureThy.add_thms
   10.22 @@ -183,7 +183,7 @@
   10.23                    [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
   10.24                  ((Abs_name ^ "_induct", make Abs_induct),
   10.25                    [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
   10.26 -            |>> Theory.parent_path;
   10.27 +            ||> Theory.parent_path;
   10.28            val result = {type_definition = type_definition, set_def = set_def,
   10.29              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
   10.30              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
    11.1 --- a/src/HOLCF/domain/axioms.ML	Thu Dec 08 20:16:17 2005 +0100
    11.2 +++ b/src/HOLCF/domain/axioms.ML	Fri Dec 09 09:06:45 2005 +0100
    11.3 @@ -111,7 +111,7 @@
    11.4      [take_def, finite_def])
    11.5  end; (* let *)
    11.6  
    11.7 -fun add_axioms_i x = #1 o PureThy.add_axioms_i (map Thm.no_attributes x);
    11.8 +fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x);
    11.9  fun add_axioms_infer axms thy = add_axioms_i (infer_types thy axms) thy;
   11.10  
   11.11  fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
    12.1 --- a/src/HOLCF/domain/extender.ML	Thu Dec 08 20:16:17 2005 +0100
    12.2 +++ b/src/HOLCF/domain/extender.ML	Fri Dec 09 09:06:45 2005 +0100
    12.3 @@ -134,7 +134,7 @@
    12.4    in
    12.5      theorems_thy
    12.6      |> Theory.add_path (Sign.base_name comp_dnam)
    12.7 -    |> (#1 o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
    12.8 +    |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
    12.9      |> Theory.parent_path
   12.10    end;
   12.11  
    13.1 --- a/src/HOLCF/domain/theorems.ML	Thu Dec 08 20:16:17 2005 +0100
    13.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Dec 09 09:06:45 2005 +0100
    13.3 @@ -353,7 +353,7 @@
    13.4                          (List.filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
    13.5  val copy_rews = copy_strict::copy_apps @ copy_stricts;
    13.6  in thy |> Theory.add_path (Sign.base_name dname)
    13.7 -       |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
    13.8 +       |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
    13.9  		("iso_rews" , iso_rews  ),
   13.10  		("exhaust"  , [exhaust] ),
   13.11  		("casedist" , [casedist]),
   13.12 @@ -368,7 +368,7 @@
   13.13  		("inverts" , inverts ),
   13.14  		("injects" , injects ),
   13.15  		("copy_rews", copy_rews)])))
   13.16 -       |> (#1 o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
   13.17 +       |> (snd o PureThy.add_thmss [(("match_rews", mat_rews), [Simplifier.simp_add_global])])
   13.18         |> Theory.parent_path |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
   13.19                   pat_rews @ dist_les @ dist_eqs @ copy_rews)
   13.20  end; (* let *)
   13.21 @@ -630,7 +630,7 @@
   13.22  end; (* local *)
   13.23  
   13.24  in thy |> Theory.add_path comp_dnam
   13.25 -       |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
   13.26 +       |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
   13.27  		("take_rews"  , take_rews  ),
   13.28  		("take_lemmas", take_lemmas),
   13.29  		("finites"    , finites    ),
    14.1 --- a/src/HOLCF/fixrec_package.ML	Thu Dec 08 20:16:17 2005 +0100
    14.2 +++ b/src/HOLCF/fixrec_package.ML	Fri Dec 09 09:06:45 2005 +0100
    14.3 @@ -120,7 +120,7 @@
    14.4          in (n^"_unfold", thmL) :: unfolds ns thmR end;
    14.5      val unfold_thms = unfolds names ctuple_unfold_thm;
    14.6      val thms = ctuple_induct_thm :: unfold_thms;
    14.7 -    val (thy'', _) = PureThy.add_thms (map Thm.no_attributes thms) thy';
    14.8 +    val (_, thy'') = PureThy.add_thms (map Thm.no_attributes thms) thy';
    14.9    in
   14.10      (thy'', names, fixdef_thms, map snd unfold_thms)
   14.11    end;
   14.12 @@ -247,13 +247,13 @@
   14.13      if strict then let (* only prove simp rules if strict = true *)
   14.14        val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts);
   14.15        val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks));
   14.16 -      val (thy'', simp_thms) = PureThy.add_thms simps thy';
   14.17 +      val (simp_thms, thy'') = PureThy.add_thms simps thy';
   14.18        
   14.19        val simp_names = map (fn name => name^"_simps") cnames;
   14.20        val simp_attribute = rpair [Simplifier.simp_add_global];
   14.21        val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
   14.22      in
   14.23 -      (#1 o PureThy.add_thmss simps') thy''
   14.24 +      (snd o PureThy.add_thmss simps') thy''
   14.25      end
   14.26      else thy'
   14.27    end;
   14.28 @@ -283,7 +283,7 @@
   14.29      val ts = map (prep_term thy) strings;
   14.30      val simps = map (fix_pat thy) ts;
   14.31    in
   14.32 -    (#1 o PureThy.add_thmss [((name, simps), atts)]) thy
   14.33 +    (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   14.34    end;
   14.35  
   14.36  val add_fixpat = gen_add_fixpat Sign.read_term Attrib.global_attribute;
    15.1 --- a/src/HOLCF/pcpodef_package.ML	Thu Dec 08 20:16:17 2005 +0100
    15.2 +++ b/src/HOLCF/pcpodef_package.ML	Fri Dec 09 09:06:45 2005 +0100
    15.3 @@ -111,7 +111,7 @@
    15.4        let
    15.5          val admissible' = option_fold_rule set_def admissible;
    15.6          val cpo_thms = [type_def, less_def, admissible'];
    15.7 -        val (theory', _) =
    15.8 +        val (_, theory') =
    15.9            theory
   15.10            |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"])
   15.11              (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
   15.12 @@ -123,14 +123,14 @@
   15.13                (("lub_"     ^ name, typedef_lub     OF cpo_thms), []),
   15.14                (("thelub_"  ^ name, typedef_thelub  OF cpo_thms), []),
   15.15                (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
   15.16 -          |>> Theory.parent_path;
   15.17 +          ||> Theory.parent_path;
   15.18        in (theory', defs) end;
   15.19  
   15.20      fun make_pcpo UUmem (theory, defs as (type_def, less_def, set_def)) =
   15.21        let
   15.22          val UUmem' = option_fold_rule set_def UUmem;
   15.23          val pcpo_thms = [type_def, less_def, UUmem'];
   15.24 -        val (theory', _) =
   15.25 +        val (_, theory') =
   15.26            theory
   15.27            |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"])
   15.28              (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
   15.29 @@ -141,7 +141,7 @@
   15.30                ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
   15.31                ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
   15.32                ])
   15.33 -          |>> Theory.parent_path;
   15.34 +          ||> Theory.parent_path;
   15.35        in (theory', defs) end;
   15.36      
   15.37      fun pcpodef_result (theory, UUmem_admissible) =
    16.1 --- a/src/Pure/Isar/calculation.ML	Thu Dec 08 20:16:17 2005 +0100
    16.2 +++ b/src/Pure/Isar/calculation.ML	Fri Dec 09 09:06:45 2005 +0100
    16.3 @@ -135,7 +135,7 @@
    16.4      ("sym", sym_attr, "declaration of symmetry rule"),
    16.5      ("symmetric", (Attrib.no_args symmetric_global, Attrib.no_args symmetric_local),
    16.6        "resolution with symmetry rule")],
    16.7 -  #1 o PureThy.add_thms
    16.8 +  snd o PureThy.add_thms
    16.9     [(("", transitive_thm), [trans_add_global]),
   16.10      (("", symmetric_thm), [sym_add_global])]];
   16.11  
    17.1 --- a/src/Pure/Isar/context_rules.ML	Thu Dec 08 20:16:17 2005 +0100
    17.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Dec 09 09:06:45 2005 +0100
    17.3 @@ -252,7 +252,7 @@
    17.4  end;
    17.5  
    17.6  val _ = Context.add_setup
    17.7 -  [#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
    17.8 +  [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query_global NONE])]];
    17.9  
   17.10  
   17.11  (* low-level modifiers *)
    18.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Dec 08 20:16:17 2005 +0100
    18.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 09 09:06:45 2005 +0100
    18.3 @@ -61,36 +61,38 @@
    18.4  fun add_axms f args thy =
    18.5    f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
    18.6  
    18.7 -val add_axioms = add_axms (#1 oo PureThy.add_axioms);
    18.8 -val add_axioms_i = #1 oo PureThy.add_axioms_i;
    18.9 +val add_axioms = add_axms (snd oo PureThy.add_axioms);
   18.10 +val add_axioms_i = snd oo PureThy.add_axioms_i;
   18.11  fun add_defs (x, args) = add_axms (snd oo PureThy.add_defs x) args;
   18.12  fun add_defs_i (x, args) = (snd oo PureThy.add_defs_i x) args;
   18.13  
   18.14  
   18.15  (* theorems *)
   18.16  
   18.17 -fun present_theorems kind (thy, named_thmss) =
   18.18 +fun present_theorems kind (named_thmss, thy) =
   18.19    conditional (kind <> "" andalso kind <> Drule.internalK) (fn () =>
   18.20      Context.setmp (SOME thy) (Present.results (kind ^ "s")) named_thmss);
   18.21  
   18.22  fun theorems kind args thy = thy
   18.23    |> PureThy.note_thmss (Drule.kind kind) (Attrib.map_facts (Attrib.global_attribute thy) args)
   18.24 -  |> tap (present_theorems kind);
   18.25 +  |> tap (present_theorems kind)
   18.26 +  |> swap;
   18.27  
   18.28  fun theorems_i kind args =
   18.29    PureThy.note_thmss_i (Drule.kind kind) args
   18.30 -  #> tap (present_theorems kind);
   18.31 +  #> tap (present_theorems kind)
   18.32 +  #> swap;
   18.33  
   18.34  fun apply_theorems args = apsnd (List.concat o map snd) o theorems "" [(("", []), args)];
   18.35  fun apply_theorems_i args = apsnd (List.concat o map snd) o theorems_i "" [(("", []), args)];
   18.36  
   18.37  fun smart_theorems kind NONE args thy = thy
   18.38        |> theorems kind args
   18.39 -      |> tap (present_theorems kind)
   18.40 +      |> tap (present_theorems kind o swap)
   18.41        |> (fn (thy, _) => (thy, ProofContext.init thy))
   18.42    | smart_theorems kind (SOME loc) args thy = thy
   18.43        |> Locale.note_thmss kind loc args
   18.44 -      |> tap (present_theorems kind o apfst #1)
   18.45 +      |> tap (present_theorems kind o swap o apfst #1)
   18.46        |> #1;
   18.47  
   18.48  fun declare_theorems opt_loc args =
    19.1 --- a/src/Pure/Isar/locale.ML	Thu Dec 08 20:16:17 2005 +0100
    19.2 +++ b/src/Pure/Isar/locale.ML	Fri Dec 09 09:06:45 2005 +0100
    19.3 @@ -1383,7 +1383,7 @@
    19.4    |> Theory.add_path (Sign.base_name name)
    19.5    |> Theory.no_base_names
    19.6    |> PureThy.note_thmss_i (Drule.kind kind) args
    19.7 -  |>> Theory.restore_naming thy;
    19.8 +  ||> Theory.restore_naming thy;
    19.9  
   19.10  
   19.11  (* accesses of interpreted theorems *)
   19.12 @@ -1415,7 +1415,7 @@
   19.13    |> Theory.qualified_names
   19.14    |> Theory.custom_accesses (global_accesses prfx)
   19.15    |> PureThy.note_thmss_i kind args
   19.16 -  |>> Theory.restore_naming thy;
   19.17 +  ||> Theory.restore_naming thy;
   19.18  
   19.19  fun local_note_accesses_i prfx args ctxt =
   19.20    ctxt
   19.21 @@ -1472,12 +1472,12 @@
   19.22                map (Attrib.global_attribute_i thy) (map inst_atts atts @ atts2)),
   19.23               [(map (Drule.standard o satisfy_protected prems o
   19.24              Element.inst_thm thy insts) ths, [])]));
   19.25 -      in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
   19.26 +      in global_note_accesses_i (Drule.kind kind) prfx args' thy |> snd end;
   19.27    in fold activate regs thy end;
   19.28  
   19.29  
   19.30 -fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
   19.31 -  | smart_note_thmss kind (SOME loc) = note_thmss_qualified kind loc;
   19.32 +fun smart_note_thmss kind NONE = swap oo PureThy.note_thmss_i (Drule.kind kind)
   19.33 +  | smart_note_thmss kind (SOME loc) = swap oo note_thmss_qualified kind loc;
   19.34  
   19.35  
   19.36  local
   19.37 @@ -1509,7 +1509,7 @@
   19.38        map (rpair [] o #1 o #1) args' ~~
   19.39        map (single o Thm.no_attributes o map export o #2) facts;
   19.40  
   19.41 -    val (thy', result) =
   19.42 +    val (result, thy') =
   19.43        thy
   19.44        |> put_facts loc args'
   19.45        |> note_thmss_registrations kind loc args'
   19.46 @@ -1643,9 +1643,10 @@
   19.47            val elemss' = change_elemss axioms elemss @
   19.48              [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
   19.49          in
   19.50 -          def_thy |> note_thmss_qualified "" aname
   19.51 -            [((introN, []), [([intro], [])])]
   19.52 -          |> #1 |> rpair (elemss', [statement])
   19.53 +          def_thy
   19.54 +          |> note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
   19.55 +          |> snd
   19.56 +          |> rpair (elemss', [statement])
   19.57          end;
   19.58      val (thy'', predicate) =
   19.59        if null ints then (thy', ([], []))
   19.60 @@ -1655,10 +1656,12 @@
   19.61              thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts);
   19.62            val cstatement = Thm.cterm_of def_thy statement;
   19.63          in
   19.64 -          def_thy |> note_thmss_qualified "" bname
   19.65 -            [((introN, []), [([intro], [])]),
   19.66 -             ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])]
   19.67 -          |> #1 |> rpair ([cstatement], axioms)
   19.68 +          def_thy
   19.69 +          |> note_thmss_qualified "" bname
   19.70 +               [((introN, []), [([intro], [])]),
   19.71 +                ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])]
   19.72 +          |> snd
   19.73 +          |> rpair ([cstatement], axioms)
   19.74          end;
   19.75    in (thy'', (elemss', predicate)) end;
   19.76  
   19.77 @@ -1707,7 +1710,7 @@
   19.78      val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'))
   19.79    in
   19.80      pred_thy
   19.81 -    |> note_thmss_qualified "" name facts' |> #1
   19.82 +    |> note_thmss_qualified "" name facts' |> snd
   19.83      |> declare_locale name
   19.84      |> put_locale name {predicate = predicate, import = import,
   19.85          elems = map (fn e => (e, stamp ())) elems',
   19.86 @@ -1883,7 +1886,7 @@
   19.87  fun global_activate_facts_elemss x = gen_activate_facts_elemss
   19.88        (fn thy => fn (name, ps) =>
   19.89          get_global_registration thy (name, map Logic.varify ps))
   19.90 -      (global_note_accesses_i (Drule.kind ""))
   19.91 +      (swap ooo global_note_accesses_i (Drule.kind ""))
   19.92        Attrib.global_attribute_i Drule.standard
   19.93        (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
   19.94        (fn (n, ps) => fn (t, th) =>
   19.95 @@ -2084,7 +2087,9 @@
   19.96                        |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
   19.97                        |> map (apfst (apfst (NameSpace.qualified prfx)))
   19.98                  in
   19.99 -                  fst (global_note_accesses_i (Drule.kind "") prfx facts' thy)
  19.100 +                  thy
  19.101 +                  |> global_note_accesses_i (Drule.kind "") prfx facts'
  19.102 +                  |> snd
  19.103                  end
  19.104                | activate_elem _ thy = thy;
  19.105  
    20.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 08 20:16:17 2005 +0100
    20.2 +++ b/src/Pure/Isar/proof.ML	Fri Dec 09 09:06:45 2005 +0100
    20.3 @@ -622,7 +622,7 @@
    20.4  
    20.5  val local_results = gen_thmss ProofContext.note_thmss_i (K []) I I (K I);
    20.6  fun global_results kind =
    20.7 -  swap oo (PureThy.note_thmss_i (Drule.kind kind) o map (apsnd Thm.simple_fact));
    20.8 +  PureThy.note_thmss_i (Drule.kind kind) o map (apsnd Thm.simple_fact);
    20.9  
   20.10  fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state);
   20.11  fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])];
    21.1 --- a/src/Pure/axclass.ML	Thu Dec 08 20:16:17 2005 +0100
    21.2 +++ b/src/Pure/axclass.ML	Fri Dec 09 09:06:45 2005 +0100
    21.3 @@ -196,20 +196,20 @@
    21.4        (map inclass super_classes @ map (int_axm o #2) axms, inclass class);
    21.5  
    21.6      (*declare axioms and rule*)
    21.7 -    val (axms_thy, ([intro], [axioms])) =
    21.8 +    val (([intro], [axioms]), axms_thy) =
    21.9        class_thy
   21.10        |> Theory.add_path (Sign.const_of_class bclass)
   21.11        |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
   21.12 -      |>>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
   21.13 +      ||>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
   21.14      val info = {super_classes = super_classes, intro = intro, axioms = axioms};
   21.15  
   21.16      (*store info*)
   21.17 -    val final_thy =
   21.18 +    val (_, final_thy) =
   21.19        axms_thy
   21.20        |> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT --> propT)]
   21.21 -      |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts))
   21.22 -      |> Theory.restore_naming class_thy
   21.23 -      |> AxclassesData.map (Symtab.update (class, info));
   21.24 +      |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
   21.25 +      ||> Theory.restore_naming class_thy
   21.26 +      ||> AxclassesData.map (Symtab.update (class, info));
   21.27    in (final_thy, {intro = intro, axioms = axioms}) end;
   21.28  
   21.29  in
    22.1 --- a/src/Pure/pure_thy.ML	Thu Dec 08 20:16:17 2005 +0100
    22.2 +++ b/src/Pure/pure_thy.ML	Fri Dec 09 09:06:45 2005 +0100
    22.3 @@ -52,23 +52,23 @@
    22.4    val smart_store_thms_open: (bstring * thm list) -> thm list
    22.5    val forall_elim_var: int -> thm -> thm
    22.6    val forall_elim_vars: int -> thm -> thm
    22.7 -  val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
    22.8 +  val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> thm list * theory
    22.9    val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
   22.10 -    -> theory * thm list list
   22.11 +    -> thm list list * theory 
   22.12    val note_thmss: theory attribute -> ((bstring * theory attribute list) *
   22.13      (thmref * theory attribute list) list) list ->
   22.14 -    theory -> theory * (bstring * thm list) list
   22.15 +    theory -> (bstring * thm list) list * theory
   22.16    val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
   22.17      (thm list * theory attribute list) list) list ->
   22.18 -    theory -> theory * (bstring * thm list) list
   22.19 +    theory -> (bstring * thm list) list * theory
   22.20    val add_axioms: ((bstring * string) * theory attribute list) list ->
   22.21 -    theory -> theory * thm list
   22.22 +    theory -> thm list * theory
   22.23    val add_axioms_i: ((bstring * term) * theory attribute list) list ->
   22.24 -    theory -> theory * thm list
   22.25 +    theory -> thm list * theory
   22.26    val add_axiomss: ((bstring * string list) * theory attribute list) list ->
   22.27 -    theory -> theory * thm list list
   22.28 +    theory -> thm list list * theory
   22.29    val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
   22.30 -    theory -> theory * thm list list
   22.31 +    theory -> thm list list * theory
   22.32    val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
   22.33      theory -> thm list * theory
   22.34    val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
   22.35 @@ -340,14 +340,14 @@
   22.36  (* add_thms(s) *)
   22.37  
   22.38  fun add_thms_atts pre_name ((bname, thms), atts) =
   22.39 -  enter_thms pre_name (name_thms false)
   22.40 +  swap o enter_thms pre_name (name_thms false)
   22.41      (Thm.applys_attributes o rpair atts) (bname, thms);
   22.42  
   22.43 -fun gen_add_thmss pre_name args theory =
   22.44 -  foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args);
   22.45 +fun gen_add_thmss pre_name =
   22.46 +  fold_map (add_thms_atts pre_name);
   22.47  
   22.48  fun gen_add_thms pre_name args =
   22.49 -  apsnd (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
   22.50 +  apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
   22.51  
   22.52  val add_thmss = gen_add_thmss (name_thms true);
   22.53  val add_thms = gen_add_thms (name_thms true);
   22.54 @@ -370,8 +370,8 @@
   22.55  
   22.56  in
   22.57  
   22.58 -val note_thmss = gen_note_thmss get_thms;
   22.59 -val note_thmss_i = gen_note_thmss (K I);
   22.60 +val note_thmss = swap ooo gen_note_thmss get_thms;
   22.61 +val note_thmss_i = swap ooo gen_note_thmss (K I);
   22.62  
   22.63  end;
   22.64  
   22.65 @@ -379,7 +379,7 @@
   22.66  (* store_thm *)
   22.67  
   22.68  fun store_thm ((bname, thm), atts) thy =
   22.69 -  let val (thy', [th']) = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy
   22.70 +  let val ([th'], thy') = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy
   22.71    in (th', thy') end;
   22.72  
   22.73  
   22.74 @@ -430,32 +430,29 @@
   22.75  local
   22.76    fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name);
   22.77    fun get_axs thy named_axs = map (forall_elim_vars 0 o get_ax thy) named_axs;
   22.78 -
   22.79 -  fun add_single add (thy, ((name, ax), atts)) =
   22.80 +  fun add_single add ((name, ax), atts) thy =
   22.81      let
   22.82        val named_ax = [(name, ax)];
   22.83        val thy' = add named_ax thy;
   22.84        val thm = hd (get_axs thy' named_ax);
   22.85 -    in apsnd hd (gen_add_thms (K I) [((name, thm), atts)] thy') end;
   22.86 -
   22.87 -  fun add_multi add (thy, ((name, axs), atts)) =
   22.88 +    in apfst hd (gen_add_thms (K I) [((name, thm), atts)] thy') end;
   22.89 +  fun add_multi add ((name, axs), atts) thy =
   22.90      let
   22.91        val named_axs = name_multi name axs;
   22.92        val thy' = add named_axs thy;
   22.93        val thms = get_axs thy' named_axs;
   22.94 -    in apsnd hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end;
   22.95 -
   22.96 -  fun add_singles add args thy = foldl_map (add_single add) (thy, args);
   22.97 -  fun add_multis add args thy = foldl_map (add_multi add) (thy, args);
   22.98 +    in apfst hd (gen_add_thmss (K I) [((name, thms), atts)] thy') end;
   22.99 +  fun add_singles add = fold_map (add_single add);
  22.100 +  fun add_multis add = fold_map (add_multi add);
  22.101  in
  22.102    val add_axioms    = add_singles Theory.add_axioms;
  22.103    val add_axioms_i  = add_singles Theory.add_axioms_i;
  22.104    val add_axiomss   = add_multis Theory.add_axioms;
  22.105    val add_axiomss_i = add_multis Theory.add_axioms_i;
  22.106 -  val add_defs      = swap ooo add_singles o Theory.add_defs;
  22.107 -  val add_defs_i    = swap ooo add_singles o Theory.add_defs_i;
  22.108 -  val add_defss     = swap ooo add_multis o Theory.add_defs;
  22.109 -  val add_defss_i   = swap ooo add_multis o Theory.add_defs_i;
  22.110 +  val add_defs      = add_singles o Theory.add_defs;
  22.111 +  val add_defs_i    = add_singles o Theory.add_defs_i;
  22.112 +  val add_defss     = add_multis o Theory.add_defs;
  22.113 +  val add_defss_i   = add_multis o Theory.add_defs_i;
  22.114  end;
  22.115  
  22.116  
  22.117 @@ -525,13 +522,13 @@
  22.118       Const ("TYPE", a_itselfT),
  22.119       Const (Term.dummy_patternN, aT)]
  22.120    |> Theory.add_modesyntax ("", false)
  22.121 -    (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
  22.122 +       (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
  22.123    |> Theory.add_trfuns Syntax.pure_trfuns
  22.124    |> Theory.add_trfunsT Syntax.pure_trfunsT
  22.125    |> Sign.local_path
  22.126 -  |> (snd oo (add_defs_i false o map Thm.no_attributes))
  22.127 -   [("prop_def", Logic.mk_equals (Logic.protect A, A))]
  22.128 -  |> (#1 o add_thmss [(("nothing", []), [])])
  22.129 +  |> (add_defs_i false o map Thm.no_attributes)
  22.130 +       [("prop_def", Logic.mk_equals (Logic.protect A, A))] |> snd
  22.131 +  |> add_thmss [(("nothing", []), [])] |> snd
  22.132    |> Theory.add_axioms_i Proofterm.equality_axms
  22.133    |> Theory.end_theory;
  22.134  
    23.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Dec 08 20:16:17 2005 +0100
    23.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Dec 09 09:06:45 2005 +0100
    23.3 @@ -366,14 +366,14 @@
    23.4   in
    23.5    (*Updating theory components: simprules and datatype info*)
    23.6    (thy1 |> Theory.add_path big_rec_base_name
    23.7 -        |> (#1 o PureThy.add_thmss
    23.8 +        |> PureThy.add_thmss
    23.9           [(("simps", simps), [Simplifier.simp_add_global]),
   23.10            (("", intrs), [Classical.safe_intro_global]),
   23.11            (("con_defs", con_defs), []),
   23.12            (("case_eqns", case_eqns), []),
   23.13            (("recursor_eqns", recursor_eqns), []),
   23.14            (("free_iffs", free_iffs), []),
   23.15 -          (("free_elims", free_SEs), [])])
   23.16 +          (("free_elims", free_SEs), [])] |> snd
   23.17          |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
   23.18          |> ConstructorsData.map (fold Symtab.update con_pairs)
   23.19          |> Theory.parent_path,
    24.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Dec 08 20:16:17 2005 +0100
    24.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Dec 09 09:06:45 2005 +0100
    24.3 @@ -165,7 +165,7 @@
    24.4    in
    24.5      thy
    24.6      |> Theory.add_path (Sign.base_name big_rec_name)
    24.7 -    |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
    24.8 +    |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> snd
    24.9      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   24.10      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   24.11      |> Theory.parent_path
    25.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Dec 08 20:16:17 2005 +0100
    25.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Dec 09 09:06:45 2005 +0100
    25.3 @@ -175,8 +175,10 @@
    25.4            else ()
    25.5  
    25.6    (*add definitions of the inductive sets*)
    25.7 -  val thy1 = thy |> Theory.add_path big_rec_base_name
    25.8 -                 |> (snd o PureThy.add_defs_i false (map Thm.no_attributes axpairs))
    25.9 +  val (_, thy1) =
   25.10 +    thy
   25.11 +    |> Theory.add_path big_rec_base_name
   25.12 +    |> PureThy.add_defs_i false (map Thm.no_attributes axpairs)
   25.13  
   25.14  
   25.15    (*fetch fp definitions from the theory*)
   25.16 @@ -510,9 +512,10 @@
   25.17                    |> standard
   25.18       and mutual_induct = CP.remove_split mutual_induct_fsplit
   25.19  
   25.20 -     val (thy', [induct', mutual_induct']) = thy |> PureThy.add_thms
   25.21 -      [((co_prefix ^ "induct", induct), [case_names, InductAttrib.induct_set_global big_rec_name]),
   25.22 -       (("mutual_induct", mutual_induct), [case_names])];
   25.23 +     val ([induct', mutual_induct'], thy') =
   25.24 +       thy
   25.25 +       |> PureThy.add_thms [((co_prefix ^ "induct", induct), [case_names, InductAttrib.induct_set_global big_rec_name]),
   25.26 +            (("mutual_induct", mutual_induct), [case_names])];
   25.27      in ((thy', induct'), mutual_induct')
   25.28      end;  (*of induction_rules*)
   25.29  
   25.30 @@ -520,23 +523,27 @@
   25.31  
   25.32    val ((thy2, induct), mutual_induct) =
   25.33      if not coind then induction_rules raw_induct thy1
   25.34 -    else (thy1 |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])] |> apsnd hd, TrueI)
   25.35 +    else
   25.36 +      (thy1
   25.37 +      |> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])]
   25.38 +      |> apfst hd |> Library.swap, TrueI)
   25.39    and defs = big_rec_def :: part_rec_defs
   25.40  
   25.41  
   25.42 -  val (thy3, ([bnd_mono', dom_subset', elim'], [defs', intrs'])) =
   25.43 +  val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) =
   25.44      thy2
   25.45      |> IndCases.declare big_rec_name make_cases
   25.46      |> PureThy.add_thms
   25.47        [(("bnd_mono", bnd_mono), []),
   25.48         (("dom_subset", dom_subset), []),
   25.49         (("cases", elim), [case_names, InductAttrib.cases_set_global big_rec_name])]
   25.50 -    |>>> (PureThy.add_thmss o map Thm.no_attributes)
   25.51 +    ||>> (PureThy.add_thmss o map Thm.no_attributes)
   25.52          [("defs", defs),
   25.53           ("intros", intrs)];
   25.54 -  val (thy4, intrs'') =
   25.55 -    thy3 |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
   25.56 -    |>> Theory.parent_path;
   25.57 +  val (intrs'', thy4) =
   25.58 +    thy3
   25.59 +    |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
   25.60 +    ||> Theory.parent_path;
   25.61    in
   25.62      (thy4,
   25.63        {defs = defs',
    26.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Dec 08 20:16:17 2005 +0100
    26.2 +++ b/src/ZF/Tools/primrec_package.ML	Fri Dec 09 09:06:45 2005 +0100
    26.3 @@ -186,10 +186,13 @@
    26.4          standard (Goal.prove thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
    26.5            (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))));
    26.6  
    26.7 -    val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
    26.8 -    val thy3 = thy2
    26.9 -      |> (#1 o PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])])
   26.10 -      |> Theory.parent_path;
   26.11 +    val (eqn_thms', thy2) =
   26.12 +      thy1
   26.13 +      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
   26.14 +    val (_, thy3) =
   26.15 +      thy2
   26.16 +      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])]
   26.17 +      ||> Theory.parent_path;
   26.18    in (thy3, eqn_thms') end;
   26.19  
   26.20  fun add_primrec args thy =