# HG changeset patch
# User wenzelm
# Date 1324067001 -3600
# Node ID cea7cd0c7e99528d91c80be03b0c6c281d734cdc
# Parent  793bf5fa5fbf0471b54fefb95e1128240c5621a6
eliminated old-fashioned Global_Theory.add_thms(s);

diff -r 793bf5fa5fbf -r cea7cd0c7e99 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 16 13:37:08 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 16 21:23:21 2011 +0100
@@ -644,11 +644,11 @@
               DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                   (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
 
-    val ([dt_induct'], thy7) =
+    val ([(_, [dt_induct'])], thy7) =
       thy6
-      |> Global_Theory.add_thms
-        [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
-          [case_names_induct])]
+      |> Global_Theory.note_thmss ""
+        [((Binding.qualify true big_name (Binding.name "induct"), [case_names_induct]),
+          [([dt_induct], [])])]
       ||> Theory.checkpoint;
 
   in
diff -r 793bf5fa5fbf -r cea7cd0c7e99 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 16 13:37:08 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Dec 16 21:23:21 2011 +0100
@@ -270,10 +270,11 @@
   in
     thy2
     |> Sign.add_path (space_implode "_" new_type_names)
-    |> Global_Theory.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
+    |> Global_Theory.note_thmss ""
+      [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])]
     ||> Sign.parent_path
     ||> Theory.checkpoint
-    |-> (fn thms => pair (reccomb_names, flat thms))
+    |-> (fn thms => pair (reccomb_names, maps #2 thms))
   end;
 
 
diff -r 793bf5fa5fbf -r cea7cd0c7e99 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 16 13:37:08 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 16 21:23:21 2011 +0100
@@ -93,29 +93,29 @@
 
 (* store theorems in theory *)
 
-fun store_thmss_atts label tnames attss thmss =
+fun store_thmss_atts name tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
-    Global_Theory.add_thmss
-      [((Binding.qualify true tname (Binding.name label), thms), atts)]
-    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
+    Global_Theory.note_thmss ""
+      [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])]
+    #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
-fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
+fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []);
 
-fun store_thms_atts label tnames attss thmss =
-  fold_map (fn ((tname, atts), thms) =>
-    Global_Theory.add_thms
-      [((Binding.qualify true tname (Binding.name label), thms), atts)]
-    #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
+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)
   ##> Theory.checkpoint;
 
-fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
+fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []);
 
 
 (* split theorem thm_1 & ... & thm_n into n theorems *)
 
 fun split_conj_thm th =
-  ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
+  ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
 
 val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
 val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
diff -r 793bf5fa5fbf -r cea7cd0c7e99 src/HOL/Tools/Datatype/rep_datatype.ML
--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Dec 16 13:37:08 2011 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Fri Dec 16 21:23:21 2011 +0100
@@ -78,25 +78,26 @@
     val dt_names = map fst dt_infos;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
     val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
-    val named_rules = flat (map_index (fn (index, tname) =>
-      [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
-       ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
+    val named_rules = flat (map_index (fn (i, tname) =>
+      [((Binding.empty, [Induct.induct_type tname]), [([nth inducts i], [])]),
+       ((Binding.empty, [Induct.cases_type tname]), [([nth exhaust i], [])])]) dt_names);
     val unnamed_rules = map (fn induct =>
-      ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
+      ((Binding.empty, [Rule_Cases.inner_rule, Induct.induct_type ""]), [([induct], [])]))
         (drop (length dt_names) inducts);
   in
     thy9
-    |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []),
-        ((prfx (Binding.name "inducts"), inducts), []),
-        ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
-        ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
-          [Simplifier.simp_add]),
-        ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
-        ((Binding.empty, flat inject), [iff_add]),
-        ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
-          [Classical.safe_elim NONE]),
-        ((Binding.empty, weak_case_congs), [Simplifier.cong_add]),
-        ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
+    |> Global_Theory.note_thmss ""
+      ([((prfx (Binding.name "simps"), []), [(simps, [])]),
+        ((prfx (Binding.name "inducts"), []), [(inducts, [])]),
+        ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]),
+        ((Binding.empty, [Simplifier.simp_add]),
+          [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]),
+        ((Binding.empty, [Code.add_default_eqn_attribute]), [(rec_rewrites, [])]),
+        ((Binding.empty, [iff_add]), [(flat inject, [])]),
+        ((Binding.empty, [Classical.safe_elim NONE]),
+          [(map (fn th => th RS notE) (flat distinct), [])]),
+        ((Binding.empty, [Simplifier.cong_add]), [(weak_case_congs, [])]),
+        ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
           named_rules @ unnamed_rules)
     |> snd
     |> Datatype_Data.register dt_infos
@@ -116,13 +117,13 @@
     val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
     val new_type_names = map Long_Name.base_name dt_names;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
-    val (((inject, distinct), [induct]), thy2) =
+    val (((inject, distinct), [(_, [induct])]), thy2) =
       thy1
       |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject
       ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct
-      ||>> Global_Theory.add_thms
-        [((prfx (Binding.name "induct"), raw_induct),
-          [Datatype_Data.mk_case_names_induct descr])];
+      ||>> Global_Theory.note_thmss ""
+        [((prfx (Binding.name "induct"), [Datatype_Data.mk_case_names_induct descr]),
+          [([raw_induct], [])])];
   in
     thy2
     |> derive_datatype_props config dt_names [descr] induct inject distinct
diff -r 793bf5fa5fbf -r cea7cd0c7e99 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Fri Dec 16 13:37:08 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Dec 16 21:23:21 2011 +0100
@@ -202,12 +202,12 @@
     val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
       prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
 
-    val ([size_thms], thy'') =
-      Global_Theory.add_thmss
-        [((Binding.name "size", size_eqns),
-          [Simplifier.simp_add, Nitpick_Simps.add,
-           Thm.declaration_attribute
-               (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy';
+    val ([(_, size_thms)], thy'') = thy'
+      |> Global_Theory.note_thmss ""
+        [((Binding.name "size",
+            [Simplifier.simp_add, Nitpick_Simps.add,
+             Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
+          [(size_eqns, [])])];
 
   in
     SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))