--- 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;
--- 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) []);
--- 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 ~~
--- 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)
--- 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,
--- 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')
--- 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;
--- 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')
--- 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
--- 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,
--- 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);
--- 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;
--- 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 ),
--- 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;
--- 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) =
--- 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])]];
--- 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 *)
--- 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 =
--- 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;
--- 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, [])])];
--- 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
--- 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;
--- 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,
--- 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
--- 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',
--- 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 =