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