--- a/src/Pure/Isar/isar_cmd.ML Mon Mar 22 15:07:07 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Mar 22 19:23:03 2010 +0100
@@ -166,7 +166,7 @@
(* old-style axioms *)
-val add_axioms = fold (fn (b, ax) => snd o Specification.axiomatization_cmd [] [(b, [ax])]);
+val add_axioms = fold (snd oo Specification.axiom_cmd);
fun add_defs ((unchecked, overloaded), args) thy =
thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded
--- a/src/Pure/Isar/specification.ML Mon Mar 22 15:07:07 2010 +0100
+++ b/src/Pure/Isar/specification.ML Mon Mar 22 19:23:03 2010 +0100
@@ -32,6 +32,8 @@
val axiomatization_cmd: (binding * string option * mixfix) list ->
(Attrib.binding * string list) list -> theory ->
(term list * thm list list) * theory
+ val axiom: Attrib.binding * term -> theory -> thm * theory
+ val axiom_cmd: Attrib.binding * string -> theory -> thm * theory
val definition:
(binding * typ option * mixfix) option * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory
@@ -187,6 +189,9 @@
val axiomatization = gen_axioms false check_specification;
val axiomatization_cmd = gen_axioms true read_specification;
+fun axiom (b, ax) = axiomatization [] [(b, [ax])] #>> (hd o hd o snd);
+fun axiom_cmd (b, ax) = axiomatization_cmd [] [(b, [ax])] #>> (hd o hd o snd);
+
(* definition *)