# HG changeset patch # User haftmann # Date 1133856249 -3600 # Node ID 0a733e11021a9e8fc581ccd27db38ccb5000528e # Parent c5030cdbf8da71bd4f2a77b0781160b4a4b2f391 re-oriented some result tuples in PureThy diff -r c5030cdbf8da -r 0a733e11021a TFL/tfl.ML --- a/TFL/tfl.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/TFL/tfl.ML Tue Dec 06 09:04:09 2005 +0100 @@ -394,7 +394,7 @@ (wfrec $ map_term_types poly_tvars R) $ functional val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M) - val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy + val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy in (thy', def) end; end; @@ -551,7 +551,7 @@ val (name,Ty) = dest_atom c val defn = mk_const_def (Theory.sign_of thy) (name, Ty, S.list_mk_abs (args,rhs)) - val (theory, [def0]) = + val ([def0], theory) = thy |> PureThy.add_defs_i false [Thm.no_attributes (fid ^ "_def", defn)] diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Import/hol4rews.ML Tue Dec 06 09:04:09 2005 +0100 @@ -473,7 +473,7 @@ val sg = sign_of thy val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm) val thm2 = standard thm1 - val (thy2,_) = PureThy.store_thm((bthm,thm2),[]) thy + val thy2 = PureThy.store_thm ((bthm, thm2), []) thy |> snd val thy5 = add_hol4_theorem bthy bthm hth thy2 in thy5 diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Import/proof_kernel.ML Tue Dec 06 09:04:09 2005 +0100 @@ -1903,7 +1903,7 @@ Replaying _ => thy | _ => Theory.add_consts_i [(constname,ctype,csyn)] thy val eq = mk_defeq constname rhs' thy1 - val (thy2,thms) = PureThy.add_defs_i false [((thmname,eq),[])] thy1 + val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1 val def_thm = hd thms val thm' = def_thm RS meta_eq_to_obj_eq_thm val (thy',th) = (thy2, thm') diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Dec 06 09:04:09 2005 +0100 @@ -233,16 +233,17 @@ (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns)) (reccomb_names ~~ recTs ~~ rec_result_Ts); - val (thy2, reccomb_defs) = thy1 |> - Theory.add_consts_i (map (fn ((name, T), T') => - (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) - (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> - (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, + val (reccomb_defs, thy2) = + thy1 + |> Theory.add_consts_i (map (fn ((name, T), T') => + (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) + (reccomb_names ~~ recTs ~~ rec_result_Ts)) + |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => + ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))) - (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>> - parent_path flat_names; + (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) + ||> parent_path flat_names; (* prove characteristic equations for primrec combinators *) @@ -319,8 +320,10 @@ Logic.mk_equals (list_comb (Const (name, caseT), fns1), list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) ))); - val (thy', [def_thm]) = thy |> - Theory.add_consts_i [decl] |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]; + val ([def_thm], thy') = + thy + |> Theory.add_consts_i [decl] + |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]; in (defs @ [def_thm], thy') end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~ @@ -416,15 +419,16 @@ val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr'); val fTs = map fastype_of fs; - val (thy', size_def_thms) = thy1 |> - Theory.add_consts_i (map (fn (s, T) => - (Sign.base_name s, T --> HOLogic.natT, NoSyn)) - (Library.drop (length (hd descr), size_names ~~ recTs))) |> - (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) => - (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), - list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))) - (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>> - parent_path flat_names; + val (size_def_thms, thy') = + thy1 + |> Theory.add_consts_i (map (fn (s, T) => + (Sign.base_name s, T --> HOLogic.natT, NoSyn)) + (Library.drop (length (hd descr), size_names ~~ recTs))) + |> (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) => + (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), + list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))) + (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) + ||> parent_path flat_names; val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Tue Dec 06 09:04:09 2005 +0100 @@ -130,11 +130,11 @@ val ind_name = Thm.name_of_thm induction; val vs = map (fn i => List.nth (pnames, i)) is; - val (thy', thm') = thy + val (thm', thy') = thy |> Theory.absolute_path |> PureThy.store_thm ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), []) - |>> Theory.restore_naming thy; + ||> Theory.restore_naming thy; val ivs = Drule.vars_of_terms [Logic.varify (DatatypeProp.make_ind [descr] sorts)]; @@ -200,10 +200,10 @@ resolve_tac prems, asm_simp_tac HOL_basic_ss])]); val exh_name = Thm.name_of_thm exhaustion; - val (thy', thm') = thy + val (thm', thy') = thy |> Theory.absolute_path |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), []) - |>> Theory.restore_naming thy; + ||> Theory.restore_naming thy; val P = Var (("P", 0), rT' --> HOLogic.boolT); val prf = forall_intr_prf (y, forall_intr_prf (P, diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Dec 06 09:04:09 2005 +0100 @@ -226,7 +226,7 @@ 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 (thy', [def_thm]) = thy |> + 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)]; @@ -368,7 +368,7 @@ val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $ list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos); - val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; + val (def_thms, thy') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; (* prove characteristic equations *) diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/inductive_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -451,7 +451,7 @@ fun cases_spec name elim thy = thy |> Theory.add_path (Sign.base_name name) - |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])]) + |> (fst 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; @@ -750,7 +750,7 @@ val def_terms = fp_def_term :: (if length cs < 2 then [] else map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs); - val (thy', [fp_def :: rec_sets_defs]) = + val ([fp_def :: rec_sets_defs], thy') = thy |> cond_declare_consts declare_consts cs paramTs cnames |> (if length cs < 2 then I diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Dec 06 09:04:09 2005 +0100 @@ -378,7 +378,7 @@ REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY' [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac, DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); - val (thy', thm') = PureThy.store_thm ((space_implode "_" + val (thm', thy') = PureThy.store_thm ((space_implode "_" (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy in Extraction.add_realizers_i @@ -426,7 +426,7 @@ rewrite_goals_tac rews, REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN' DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]); - val (thy', thm') = PureThy.store_thm ((space_implode "_" + val (thm', thy') = PureThy.store_thm ((space_implode "_" (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy in Extraction.add_realizers_i diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/primrec_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -247,7 +247,7 @@ val nameTs2 = map fst rec_eqns; val primrec_name = if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name; - val (thy', defs_thms') = thy |> Theory.add_path primrec_name |> + val (defs_thms', thy') = thy |> Theory.add_path primrec_name |> (if eq_set (nameTs1, nameTs2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs' else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^ "\nare not mutually recursive")); diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/record_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -1350,8 +1350,8 @@ |> extension_typedef name repT (alphas@[zeta]) |>> 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)) - |>>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs) + |>>> (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) 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; @@ -1748,10 +1748,10 @@ (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 - |>>> (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] + |> ((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) val (defs_thy,((sel_defs,upd_defs),derived_defs)) = timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" mk_defs; diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/specification_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -38,7 +38,7 @@ else thname val def_eq = Logic.mk_equals (Const(cname_full,ctype), HOLogic.choice_const ctype $ P) - val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy + val (thms, thy') = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy val thm' = [thm,hd thms] MRS exE_some in mk_definitional cos (thy',thm') @@ -191,18 +191,19 @@ fun undo_imps thm = equal_elim (symmetric rew_imp) thm - fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts) - fun add_final (arg as (thy,thm)) = + fun apply_atts arg = Thm.apply_attributes (arg, map (Attrib.global_attribute thy) atts) + fun add_final (arg as (thy, thm)) = if name = "" - then arg + then arg |> Library.swap else (writeln (" " ^ name ^ ": " ^ (string_of_thm thm)); - PureThy.store_thm((name,thm),[]) thy) + PureThy.store_thm ((name, thm), []) thy) in args |> apsnd (remove_alls frees) |> apsnd undo_imps |> apsnd standard |> apply_atts |> add_final + |> Library.swap end fun process_all [proc_arg] args = diff -r c5030cdbf8da -r 0a733e11021a src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOL/Tools/typedef_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -141,6 +141,15 @@ val typedef_prop = Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); + fun add_def def def' thy = + if def + then + thy + |> PureThy.add_defs_i false [Thm.no_attributes def'] + |-> (fn [def'] => pair (SOME def')) + else + (NONE, thy); + fun typedef_result (theory, nonempty) = theory |> put_typedef newT oldT (full Abs_name) (full Rep_name) @@ -149,13 +158,11 @@ ((if def then [(name, setT', NoSyn)] else []) @ [(Rep_name, newT --> oldT, NoSyn), (Abs_name, oldT --> newT, NoSyn)]) - |> (if def then (apsnd (SOME o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes)) - [Logic.mk_defpair (setC, set)] - else rpair NONE) - |>>> 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 (theory', (set_def, [type_definition])) => + |> 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) + ||> 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, diff -r c5030cdbf8da -r 0a733e11021a src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -1,19 +1,19 @@ (* Title: HOLCF/IOA/meta_theory/ioa_package.ML ID: $Id$ - Author: Tobias Hamberger, TU Muenchen + Author: Tobias Hamberger, TU Muenchen *) signature IOA_PACKAGE = sig - val add_ioa: string -> string -> - (string) list -> (string) list -> (string) list -> - (string * string) list -> string -> - (string * string * (string * string)list) list - -> theory -> theory - val add_composition : string -> (string)list -> theory -> theory - val add_hiding : string -> string -> (string)list -> theory -> theory - val add_restriction : string -> string -> (string)list -> theory -> theory - val add_rename : string -> string -> string -> theory -> theory + val add_ioa: string -> string + -> (string) list -> (string) list -> (string) list + -> (string * string) list -> string + -> (string * string * (string * string)list) list + -> theory -> theory + val add_composition : string -> (string)list -> theory -> theory + val add_hiding : string -> string -> (string)list -> theory -> theory + val add_restriction : string -> string -> (string)list -> theory -> theory + val add_rename : string -> string -> string -> theory -> theory end; structure IoaPackage: IOA_PACKAGE = @@ -353,7 +353,7 @@ (automaton_name ^ "_trans", "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes)) +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) [(automaton_name ^ "_initial_def", automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), (automaton_name ^ "_asig_def", @@ -394,7 +394,7 @@ Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) ,NoSyn)] -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes)) +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) [(automaton_name ^ "_def", automaton_name ^ " == " ^ comp_list)] end) @@ -409,7 +409,7 @@ thy |> ContConsts.add_consts_i [(automaton_name, auttyp,NoSyn)] -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes)) +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) [(automaton_name ^ "_def", automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] end) @@ -423,7 +423,7 @@ thy |> ContConsts.add_consts_i [(automaton_name, auttyp,NoSyn)] -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes)) +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) [(automaton_name ^ "_def", automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] end) @@ -449,7 +449,7 @@ Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) ,NoSyn)] -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes)) +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] end) diff -r c5030cdbf8da -r 0a733e11021a src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOLCF/domain/axioms.ML Tue Dec 06 09:04:09 2005 +0100 @@ -114,7 +114,7 @@ fun add_axioms_i x = #1 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 = #1 o (PureThy.add_defs_i false) (map Thm.no_attributes x); +fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x); fun add_defs_infer defs thy = add_defs_i (infer_types thy defs) thy; in (* local *) diff -r c5030cdbf8da -r 0a733e11021a src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOLCF/fixrec_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -101,7 +101,7 @@ val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint); val fixdefs = map (inferT_axm thy) pre_fixdefs; - val (thy', fixdef_thms) = + val (fixdef_thms, thy') = PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy; val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms; diff -r c5030cdbf8da -r 0a733e11021a src/HOLCF/pcpodef_package.ML --- a/src/HOLCF/pcpodef_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/HOLCF/pcpodef_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -95,17 +95,17 @@ fun option_fold_rule NONE = I | option_fold_rule (SOME def) = fold_rule [def]; - fun make_po tac theory = - theory + fun make_po tac thy = + thy |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac |>> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.sq_ord"]) - (AxClass.intro_classes_tac []) - |>>> PureThy.add_defs_i true [Thm.no_attributes less_def] - |> (fn (theory', ({type_definition, set_def, ...}, [less_definition])) => - theory' - |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.po"]) - (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) - |> rpair (type_definition, less_definition, set_def)); + (AxClass.intro_classes_tac []) + |>>> (PureThy.add_defs_i true [Thm.no_attributes less_def] #> Library.swap) + |> (fn (thy', ({type_definition, set_def, ...}, [less_definition])) => + thy' + |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.po"]) + (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) + |> rpair (type_definition, less_definition, set_def)); fun make_cpo admissible (theory, defs as (type_def, less_def, set_def)) = let @@ -178,11 +178,11 @@ gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([], [])) thy end; -val pcpodef_proof = gen_pcpodef_proof read_term true; -val pcpodef_proof_i = gen_pcpodef_proof cert_term true; +fun pcpodef_proof x = gen_pcpodef_proof read_term true x; +fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x; -val cpodef_proof = gen_pcpodef_proof read_term false; -val cpodef_proof_i = gen_pcpodef_proof cert_term false; +fun cpodef_proof x = gen_pcpodef_proof read_term false x; +fun cpodef_proof_i x = gen_pcpodef_proof cert_term false x; (** outer syntax **) diff -r c5030cdbf8da -r 0a733e11021a src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/Pure/Isar/constdefs.ML Tue Dec 06 09:04:09 2005 +0100 @@ -66,7 +66,8 @@ val thy' = thy |> Theory.add_consts_i [(c, T, mx)] - |> PureThy.add_defs_i false [((name, def), atts)] |> #1; + |> PureThy.add_defs_i false [((name, def), atts)] + |> snd; in ((c, T), thy') end; fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy = diff -r c5030cdbf8da -r 0a733e11021a src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/Pure/Isar/isar_thy.ML Tue Dec 06 09:04:09 2005 +0100 @@ -63,8 +63,8 @@ val add_axioms = add_axms (#1 oo PureThy.add_axioms); val add_axioms_i = #1 oo PureThy.add_axioms_i; -fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) args; -fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) args; +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 *) diff -r c5030cdbf8da -r 0a733e11021a src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/Pure/Isar/locale.ML Tue Dec 06 09:04:09 2005 +0100 @@ -1589,7 +1589,7 @@ val head = Term.list_comb (Const (name, predT), args); val statement = ObjectLogic.ensure_propT thy head; - val (defs_thy, [pred_def]) = + val ([pred_def], defs_thy) = thy |> (if bodyT <> propT then I else Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), [])) diff -r c5030cdbf8da -r 0a733e11021a src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/Pure/Proof/extraction.ML Tue Dec 06 09:04:09 2005 +0100 @@ -736,10 +736,10 @@ val fu = Type.freeze u; val thy' = if t = nullt then thy else thy |> Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |> - fst o PureThy.add_defs_i false [((extr_name s vs ^ "_def", + snd o PureThy.add_defs_i false [((extr_name s vs ^ "_def", Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]; in - fst (PureThy.store_thm ((corr_name s vs, + snd (PureThy.store_thm ((corr_name s vs, Thm.varifyT (funpow (length (term_vars corr_prop)) (forall_elim_var 0) (forall_intr_frees (ProofChecker.thm_of_proof thy' diff -r c5030cdbf8da -r 0a733e11021a src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/Pure/pure_thy.ML Tue Dec 06 09:04:09 2005 +0100 @@ -47,7 +47,7 @@ val thms_of: theory -> (string * thm) list val all_thms_of: theory -> (string * thm) list val hide_thms: bool -> string list -> theory -> theory - val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm + val store_thm: (bstring * thm) * theory attribute list -> theory -> thm * theory val smart_store_thms: (bstring * thm list) -> thm list val smart_store_thms_open: (bstring * thm list) -> thm list val forall_elim_var: int -> thm -> thm @@ -70,13 +70,13 @@ val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list val add_defs: bool -> ((bstring * string) * theory attribute list) list -> - theory -> theory * thm list + theory -> thm list * theory val add_defs_i: bool -> ((bstring * term) * theory attribute list) list -> - theory -> theory * thm list + theory -> thm list * theory val add_defss: bool -> ((bstring * string list) * theory attribute list) list -> - theory -> theory * thm list list + theory -> thm list list * theory val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list -> - theory -> theory * thm list list + theory -> thm list list * theory val generic_setup: string -> theory -> theory val add_oracle: bstring * string * string -> theory -> theory end; @@ -380,7 +380,7 @@ fun store_thm ((bname, thm), atts) thy = let val (thy', [th']) = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy - in (thy', th') end; + in (th', thy') end; (* smart_store_thms(_open) *) @@ -452,10 +452,10 @@ 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 = 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; + 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; end; @@ -529,7 +529,7 @@ |> Theory.add_trfuns Syntax.pure_trfuns |> Theory.add_trfunsT Syntax.pure_trfunsT |> Sign.local_path - |> (#1 oo (add_defs_i false o map Thm.no_attributes)) + |> (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", []), [])]) |> Theory.add_axioms_i Proofterm.equality_axms diff -r c5030cdbf8da -r 0a733e11021a src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/ZF/Tools/datatype_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -231,10 +231,10 @@ if need_recursor then thy |> Theory.add_consts_i [(recursor_base_name, recursor_typ, NoSyn)] - |> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def]) + |> (snd o PureThy.add_defs_i false [Thm.no_attributes recursor_def]) else thy; - val (thy0, con_defs) = thy_path + val (con_defs, thy0) = thy_path |> Theory.add_consts_i ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)) @@ -243,8 +243,8 @@ (case_def :: List.concat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) - |>> add_recursor - |>> Theory.parent_path + ||> add_recursor + ||> Theory.parent_path val intr_names = map #2 (List.concat con_ty_lists); val (thy1, ind_result) = diff -r c5030cdbf8da -r 0a733e11021a src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/ZF/Tools/inductive_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -176,7 +176,7 @@ (*add definitions of the inductive sets*) val thy1 = thy |> Theory.add_path big_rec_base_name - |> (#1 o PureThy.add_defs_i false (map Thm.no_attributes axpairs)) + |> (snd o PureThy.add_defs_i false (map Thm.no_attributes axpairs)) (*fetch fp definitions from the theory*) diff -r c5030cdbf8da -r 0a733e11021a src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Tue Dec 06 06:22:14 2005 +0100 +++ b/src/ZF/Tools/primrec_package.ML Tue Dec 06 09:04:09 2005 +0100 @@ -175,7 +175,7 @@ foldr (process_eqn thy) NONE eqn_terms; val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); - val (thy1, [def_thm]) = thy + val ([def_thm], thy1) = thy |> Theory.add_path (Sign.base_name fname) |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];