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