# HG changeset patch # User wenzelm # Date 1269215336 -3600 # Node ID f81557a124d56a257280cab60f169415e95609f1 # Parent e7d004b89ca8986931d9d3ae302bdbab298133de replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless; diff -r e7d004b89ca8 -r f81557a124d5 src/HOL/Boogie/Tools/boogie_loader.ML --- a/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 21 22:24:04 2010 +0100 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Mon Mar 22 00:48:56 2010 +0100 @@ -241,7 +241,7 @@ let val (used, new) = mark_axioms thy (name_axioms axs) in thy - |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) new) + |> fold_map (Drule.add_axiom o apfst Binding.name) new |-> Context.theory_map o fold Boogie_Axioms.add_thm |> log verbose "The following axioms were added:" (map fst new) |> (fn thy' => log verbose "The following axioms already existed:" diff -r e7d004b89ca8 -r f81557a124d5 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Sun Mar 21 22:24:04 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Mar 22 00:48:56 2010 +0100 @@ -182,8 +182,8 @@ val new_defs = map new_def assms val (definition, thy') = thy |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] - |> PureThy.add_axioms (map_index - (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), t), [])) new_defs) + |> fold_map Drule.add_axiom (map_index + (fn (i, t) => (Binding.name (constname ^ "_def" ^ string_of_int i), t)) new_defs) in (lhs, ((full_constname, definition) :: defs, thy')) end diff -r e7d004b89ca8 -r f81557a124d5 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Sun Mar 21 22:24:04 2010 +0100 +++ b/src/HOL/Tools/choice_specification.ML Mon Mar 22 00:48:56 2010 +0100 @@ -44,9 +44,9 @@ let fun process [] (thy,tm) = let - val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy + val (thm, thy') = Drule.add_axiom (Binding.name axname, HOLogic.mk_Trueprop tm) thy in - (thy',hd thms) + (thy', thm) end | process ((thname,cname,covld)::cos) (thy,tm) = case tm of diff -r e7d004b89ca8 -r f81557a124d5 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Sun Mar 21 22:24:04 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Mon Mar 22 00:48:56 2010 +0100 @@ -54,13 +54,8 @@ val abs_iso_bind = Binding.qualified true "abs_iso" dbind; val rep_iso_bind = Binding.qualified true "rep_iso" dbind; - val (abs_iso_thm, thy) = - yield_singleton PureThy.add_axioms - ((abs_iso_bind, abs_iso_eqn), []) thy; - - val (rep_iso_thm, thy) = - yield_singleton PureThy.add_axioms - ((rep_iso_bind, rep_iso_eqn), []) thy; + val (abs_iso_thm, thy) = Drule.add_axiom (abs_iso_bind, abs_iso_eqn) thy; + val (rep_iso_thm, thy) = Drule.add_axiom (rep_iso_bind, rep_iso_eqn) thy; val result = { @@ -88,9 +83,7 @@ val lub_take_bind = Binding.qualified true "lub_take" dbind; - val (lub_take_thm, thy) = - yield_singleton PureThy.add_axioms - ((lub_take_bind, lub_take_eqn), []) thy; + val (lub_take_thm, thy) = Drule.add_axiom (lub_take_bind, lub_take_eqn) thy; in (lub_take_thm, thy) end; diff -r e7d004b89ca8 -r f81557a124d5 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sun Mar 21 22:24:04 2010 +0100 +++ b/src/Pure/axclass.ML Mon Mar 22 00:48:56 2010 +0100 @@ -521,7 +521,7 @@ val names = name args; in thy - |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs)) + |> fold_map Drule.add_axiom (map Binding.name names ~~ specs) |-> fold add end; diff -r e7d004b89ca8 -r f81557a124d5 src/Pure/drule.ML --- a/src/Pure/drule.ML Sun Mar 21 22:24:04 2010 +0100 +++ b/src/Pure/drule.ML Mon Mar 22 00:48:56 2010 +0100 @@ -77,6 +77,7 @@ val flexflex_unique: thm -> thm val export_without_context: thm -> thm val export_without_context_open: thm -> thm + val add_axiom: (binding * term) -> theory -> thm * theory val store_thm: binding -> thm -> thm val store_standard_thm: binding -> thm -> thm val store_thm_open: binding -> thm -> thm @@ -320,6 +321,12 @@ #> Thm.close_derivation; +(* old-style axioms *) + +fun add_axiom (b, prop) = + Thm.add_axiom (b, prop) #-> (fn thm => PureThy.add_thm ((b, export_without_context thm), [])); + + (*Convert all Vars in a theorem to Frees. Also return a function for reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. Similar code in type/freeze_thaw*) diff -r e7d004b89ca8 -r f81557a124d5 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sun Mar 21 22:24:04 2010 +0100 +++ b/src/Pure/pure_thy.ML Mon Mar 22 00:48:56 2010 +0100 @@ -32,7 +32,6 @@ 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 add_axioms: ((binding * term) * attribute list) list -> theory -> thm 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 -> @@ -201,18 +200,14 @@ (* store axioms as theorems *) local - fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b); - fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs; - fun add_axm add = fold_map (fn ((b, ax), atts) => fn thy => + fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy => let - val named_ax = [(b, ax)]; - val thy' = add named_ax thy; - val thm = hd (get_axs thy' named_ax); + val thy' = add [(b, prop)] thy; + val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b)); in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end); in val add_defs = add_axm o Theory.add_defs_i false; val add_defs_unchecked = add_axm o Theory.add_defs_i true; - val add_axioms = add_axm Theory.add_axioms_i; val add_defs_cmd = add_axm o Theory.add_defs false; val add_defs_unchecked_cmd = add_axm o Theory.add_defs true; end; @@ -367,6 +362,6 @@ #> Sign.hide_const false "Pure.sort_constraint" #> Sign.hide_const false "Pure.conjunction" #> add_thmss [((Binding.name "nothing", []), [])] #> snd - #> Theory.add_axioms_i (map (apfst Binding.name) Proofterm.equality_axms))); + #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms)); end;