# HG changeset patch
# User wenzelm
# Date 1519415746 -3600
# Node ID 041898537c1961a17e1a713d2c9eeec657b4468c
# Parent  350f0579d343b2d90c83f6474f856d2d45e1f965
tuned signature;

diff -r 350f0579d343 -r 041898537c19 src/HOL/Tools/Function/function.ML
--- 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
 
diff -r 350f0579d343 -r 041898537c19 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- 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)
diff -r 350f0579d343 -r 041898537c19 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- 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) []);
 
diff -r 350f0579d343 -r 041898537c19 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- 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;
 
 
diff -r 350f0579d343 -r 041898537c19 src/Pure/Isar/expression.ML
--- 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'''') =
diff -r 350f0579d343 -r 041898537c19 src/Pure/Isar/proof.ML
--- 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);
diff -r 350f0579d343 -r 041898537c19 src/Pure/Isar/proof_context.ML
--- 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)
diff -r 350f0579d343 -r 041898537c19 src/Pure/global_theory.ML
--- 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 *)