# 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))