# HG changeset patch
# User wenzelm
# Date 1269282183 -3600
# Node ID ab6dc4d86ea11edd3355480ab06a64cd7b7cc179
# Parent  02595d4a3a7c48eaf110b498d3bea8dc79c0919f
added Specification.axiom convenience;

diff -r 02595d4a3a7c -r ab6dc4d86ea1 src/Pure/Isar/isar_cmd.ML
--- 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
diff -r 02595d4a3a7c -r ab6dc4d86ea1 src/Pure/Isar/specification.ML
--- 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 *)