--- 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;