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