--- a/src/Pure/more_thm.ML Mon Mar 22 00:48:56 2010 +0100
+++ b/src/Pure/more_thm.ML Mon Mar 22 00:51:18 2010 +0100
@@ -337,8 +337,8 @@
val (strip, recover, prop') = stripped_sorts thy prop;
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
- val thy' = thy
- |> Theory.add_axioms_i [(b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop'))];
+ val thy' =
+ Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
val axm' = Thm.axiom thy' (Sign.full_name thy' b');
val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
in (thm, thy') end;
--- a/src/Pure/theory.ML Mon Mar 22 00:48:56 2010 +0100
+++ b/src/Pure/theory.ML Mon Mar 22 00:51:18 2010 +0100
@@ -28,8 +28,7 @@
val at_end: (theory -> theory option) -> theory -> theory
val begin_theory: string -> theory list -> theory
val end_theory: theory -> theory
- val add_axioms_i: (binding * term) list -> theory -> theory
- val add_axioms: (binding * string) list -> theory -> theory
+ val add_axiom: binding * term -> theory -> theory
val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
@@ -171,23 +170,14 @@
cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
-(* add_axioms(_i) *)
+(* add_axiom *)
-local
-
-fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
+fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
let
- val axms = map (apsnd Logic.varify_global o prep_axm thy) raw_axms;
- val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
+ val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
+ val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms;
in axioms' end);
-in
-
-val add_axioms_i = gen_add_axioms cert_axm;
-val add_axioms = gen_add_axioms read_axm;
-
-end;
-
(** add constant definitions **)
@@ -269,7 +259,7 @@
let val axms = map (prep_axm thy) raw_axms in
thy
|> map_defs (fold (check_def thy unchecked overloaded) axms)
- |> add_axioms_i axms
+ |> fold add_axiom axms
end;
in