--- a/src/HOL/Tools/Function/function.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/HOL/Tools/Function/function.ML Fri Feb 23 20:55:46 2018 +0100
@@ -235,13 +235,13 @@
val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
in
lthy
- |> Proof_Context.note_thmss ""
- [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
- |> Proof_Context.note_thmss ""
- [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
- |> Proof_Context.note_thmss ""
- [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
- [([Goal.norm_result lthy termination], [])])] |> snd
+ |> Proof_Context.note_thms ""
+ ((Binding.empty, [Context_Rules.rule_del]), [([allI], [])]) |> snd
+ |> Proof_Context.note_thms ""
+ ((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])]) |> snd
+ |> Proof_Context.note_thms ""
+ ((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
+ [([Goal.norm_result lthy termination], [])]) |> snd
|> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
end
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Feb 23 20:55:46 2018 +0100
@@ -301,8 +301,8 @@
SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i;
val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
val (_, transfer_lthy) =
- Proof_Context.note_thmss ""
- [(Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])])] lthy
+ Proof_Context.note_thms ""
+ (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])]) lthy
val f_alt_def = Goal.prove_sorry transfer_lthy [] [] f_alt_def_goal
(fn {context = ctxt, prems = _} => HEADGOAL (f_alt_def_tac ctxt))
|> Thm.close_derivation
@@ -451,9 +451,10 @@
rtac ctxt TrueI] i;
val (_, transfer_lthy) =
- Proof_Context.note_thmss "" [(Binding.empty_atts,
- [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
- (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])])] lthy;
+ Proof_Context.note_thms ""
+ (Binding.empty_atts,
+ [(@{thms right_total_UNIV_transfer}, [Transfer.transfer_add]),
+ (@{thms Domain_eq_top}, [Transfer.transfer_domain_add])]) lthy;
val quot_thm_isom = Goal.prove_sorry transfer_lthy [] [] typedef_goal
(fn {context = ctxt, prems = _} => typ_isom_tac ctxt 1)
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Feb 23 20:55:46 2018 +0100
@@ -95,17 +95,17 @@
fun store_thmss_atts name tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Global_Theory.note_thmss ""
- [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])]
- #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss);
+ Global_Theory.note_thms ""
+ ((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])
+ #-> (fn (_, res) => pair res)) (tnames ~~ attss ~~ thmss);
fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []);
fun store_thms_atts name tnames attss thms =
fold_map (fn ((tname, atts), thm) =>
- Global_Theory.note_thmss ""
- [((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])]
- #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms);
+ Global_Theory.note_thms ""
+ ((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])
+ #-> (fn (_, [res]) => pair res)) (tnames ~~ attss ~~ thms);
fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []);
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Feb 23 20:55:46 2018 +0100
@@ -271,11 +271,10 @@
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
- |> Global_Theory.note_thmss ""
- [((Binding.name "rec", [Named_Theorems.add @{named_theorems nitpick_simp}]),
- [(rec_thms, [])])]
+ |> Global_Theory.note_thms ""
+ ((Binding.name "rec", [Named_Theorems.add @{named_theorems nitpick_simp}]), [(rec_thms, [])])
||> Sign.parent_path
- |-> (fn thms => pair (reccomb_names, maps #2 thms))
+ |-> (fn (_, thms) => pair (reccomb_names, thms))
end;
--- a/src/Pure/Isar/expression.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/Pure/Isar/expression.ML Fri Feb 23 20:55:46 2018 +0100
@@ -743,8 +743,8 @@
val (_, thy'') =
thy'
|> Sign.qualified_path true abinding
- |> Global_Theory.note_thmss ""
- [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
+ |> Global_Theory.note_thms ""
+ ((Binding.name introN, []), [([intro], [Locale.unfold_add])])
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
val (b_pred, b_intro, b_axioms, thy'''') =
--- a/src/Pure/Isar/proof.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/Pure/Isar/proof.ML Fri Feb 23 20:55:46 2018 +0100
@@ -1059,8 +1059,8 @@
val ctxt'' =
ctxt'
|> not (null assumes_propss) ?
- (snd o Proof_Context.note_thmss ""
- [((Binding.name Auto_Bind.thatN, []), [(prems, [])])])
+ (snd o Proof_Context.note_thms ""
+ ((Binding.name Auto_Bind.thatN, []), [(prems, [])]))
|> (snd o Proof_Context.note_thmss ""
(assumes_bindings ~~ map (map (fn th => ([th], []))) premss))
in (prems, ctxt'') end);
--- a/src/Pure/Isar/proof_context.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Feb 23 20:55:46 2018 +0100
@@ -131,6 +131,8 @@
val add_thms_dynamic: binding * (Context.generic -> thm list) ->
Proof.context -> string * Proof.context
val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context
+ val note_thms: string -> Thm.binding * (thm list * attribute list) list ->
+ Proof.context -> (string * thm list) * Proof.context
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
@@ -1079,7 +1081,7 @@
val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
in ctxt' end;
-fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn ctxt =>
+fun note_thms kind ((b, more_atts), facts) ctxt =
let
val name = full_name ctxt b;
val facts' = Global_Theory.name_thmss false name facts;
@@ -1088,7 +1090,9 @@
val (res, ctxt') = fold_map app facts' ctxt;
val thms = Global_Theory.name_thms false false name (flat res);
val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
- in ((name, thms), ctxt'') end);
+ in ((name, thms), ctxt'') end;
+
+val note_thmss = fold_map o note_thms;
fun put_thms index thms ctxt = ctxt
|> map_naming (K Name_Space.local_naming)
--- a/src/Pure/global_theory.ML Fri Feb 23 19:53:39 2018 +0100
+++ b/src/Pure/global_theory.ML Fri Feb 23 20:55:46 2018 +0100
@@ -34,8 +34,10 @@
val add_thms_dynamic': Context.generic -> binding * (Context.generic -> thm list) ->
theory -> string * theory
val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
- val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
- -> theory -> (string * thm list) list * theory
+ val note_thms: string -> Thm.binding * (thm list * attribute list) list -> theory ->
+ (string * thm list) * theory
+ val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> theory ->
+ (string * thm list) list * theory
val add_defs: bool -> ((binding * term) * attribute list) list ->
theory -> thm list * theory
val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
@@ -188,7 +190,7 @@
(* note_thmss *)
-fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy =>
+fun note_thms kind ((b, more_atts), facts) thy =
let
val name = Sign.full_name thy b;
fun app (ths, atts) =
@@ -196,7 +198,9 @@
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);
+ in ((name, thms), thy') end;
+
+val note_thmss = fold_map o note_thms;
(* old-style defs *)