--- a/src/HOL/Tools/choice_specification.ML Sat Mar 03 18:18:39 2012 +0100
+++ b/src/HOL/Tools/choice_specification.ML Sat Mar 03 21:43:59 2012 +0100
@@ -185,20 +185,21 @@
fun undo_imps thm =
Thm.equal_elim (Thm.symmetric rew_imp) thm
- fun add_final (arg as (thy, thm)) =
+ fun add_final (thm, thy) =
if name = ""
- then arg |> Library.swap
+ then (thm, thy)
else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
Global_Theory.store_thm (Binding.name name, thm) thy)
in
- args |> apsnd (remove_alls frees)
- |> apsnd undo_imps
- |> apsnd Drule.export_without_context
- |> Thm.theory_attributes
+ swap args
+ |> apfst (remove_alls frees)
+ |> apfst undo_imps
+ |> apfst Drule.export_without_context
+ |-> Thm.theory_attributes
(map (Attrib.attribute thy)
(@{attributes [nitpick_choice_spec]} @ atts))
|> add_final
- |> Library.swap
+ |> swap
end
fun process_all [proc_arg] args =
--- a/src/Pure/Isar/attrib.ML Sat Mar 03 18:18:39 2012 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Mar 03 21:43:59 2012 +0100
@@ -191,8 +191,7 @@
Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
let
val atts = map (attribute_i thy) srcs;
- val (context', th') =
- Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm);
+ val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context);
in (context', pick "" [th']) end)
||
(Scan.ahead Args.alt_name -- Args.named_fact get_fact
@@ -204,8 +203,8 @@
let
val ths = Facts.select thmref fact;
val atts = map (attribute_i thy) srcs;
- val (context', ths') =
- Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths);
+ val (ths', context') =
+ fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
in (context', pick name ths') end)
end);
--- a/src/Pure/Isar/method.ML Sat Mar 03 18:18:39 2012 +0100
+++ b/src/Pure/Isar/method.ML Sat Mar 03 21:43:59 2012 +0100
@@ -377,13 +377,12 @@
local
fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
-fun app (f, att) (context, ths) =
- Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths);
+fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context);
in
fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
- (fn (m, ths) => Scan.succeed (app m (context, ths))));
+ (fn (m, ths) => Scan.succeed (swap (app m ths context))));
fun sections ss = Scan.repeat (section ss);
--- a/src/Pure/Isar/proof_context.ML Sat Mar 03 18:18:39 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Mar 03 21:43:59 2012 +0100
@@ -894,13 +894,12 @@
in
-fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
+fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt =>
let
val name = full_name ctxt b;
val facts = Global_Theory.name_thmss false name raw_facts;
- fun app (th, attrs) x =
- swap (Library.foldl_map
- (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
+ fun app (ths, atts) =
+ fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
val (res, ctxt') = fold_map app facts ctxt;
val thms = Global_Theory.name_thms false false name (flat res);
val Mode {stmt, ...} = get_mode ctxt;
--- a/src/Pure/global_theory.ML Sat Mar 03 18:18:39 2012 +0100
+++ b/src/Pure/global_theory.ML Sat Mar 03 21:43:59 2012 +0100
@@ -80,7 +80,7 @@
(* forked proofs *)
-fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (add_proofs thms))) thy, thms);
+fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy);
val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs)));
val join_recent_proofs = force_proofs o #1 o #2 o Data.get;
@@ -153,13 +153,12 @@
fun enter_thms pre_name post_name app_att (b, thms) thy =
if Binding.is_empty b
- then swap (register_proofs (app_att (thy, thms)))
+ then app_att thms thy |-> register_proofs
else
let
val naming = Sign.naming_of thy;
val name = Name_Space.full_name naming b;
- val (thy', thms') =
- register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+ val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
val thms'' = map (Thm.transfer thy') thms';
val thy'' = thy'
|> (Data.map o apfst)
@@ -170,19 +169,18 @@
(* store_thm(s) *)
fun store_thms (b, thms) =
- enter_thms (name_thms true true) (name_thms false true) I (b, thms);
+ enter_thms (name_thms true true) (name_thms false true) pair (b, thms);
fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
fun store_thm_open (b, th) =
- enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
+ enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single;
(* add_thms(s) *)
fun add_thms_atts pre_name ((b, thms), atts) =
- enter_thms pre_name (name_thms false true)
- (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
+ enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms);
fun gen_add_thmss pre_name =
fold_map (add_thms_atts pre_name);
@@ -204,13 +202,14 @@
(* note_thmss *)
-fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
+fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy =>
let
val name = Sign.full_name thy b;
- fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
- val (thms, thy') = thy |> enter_thms
- (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
- (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
+ fun app (ths, atts) =
+ fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
+ val (thms, thy') =
+ enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app)
+ (b, facts) thy;
in ((name, thms), thy') end);
--- a/src/Pure/more_thm.ML Sat Mar 03 18:18:39 2012 +0100
+++ b/src/Pure/more_thm.ML Sat Mar 03 21:43:59 2012 +0100
@@ -73,10 +73,10 @@
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
- val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm
+ val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
- val theory_attributes: attribute list -> theory * thm -> theory * thm
- val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
+ val theory_attributes: attribute list -> thm -> theory -> thm * theory
+ val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
val no_attributes: 'a -> 'a * 'b list
val simple_fact: 'a -> ('a * 'b list) list
val tag_rule: Properties.entry -> thm -> thm
@@ -403,16 +403,16 @@
fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
-fun apply_attribute (att: attribute) (x, th) =
+fun apply_attribute (att: attribute) th x =
let val (x', th') = att (x, th)
- in (the_default x x', the_default th th') end;
+ in (the_default th th', the_default x x') end;
-fun attribute_declaration att th x = #1 (apply_attribute att (x, th));
+fun attribute_declaration att th x = #2 (apply_attribute att th x);
fun apply_attributes mk dest =
let
- fun app [] = I
- | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts;
+ fun app [] th x = (th, x)
+ | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
in app end;
val theory_attributes = apply_attributes Context.Theory Context.the_theory;