# HG changeset patch
# User wenzelm
# Date 1269196105 -3600
# Node ID 4e3fe0b8687bd2e7832bcadb821124f2016255cb
# Parent  5c5f08f6d6e4d0b1c3f5ac752e141e0a80c61d7c
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';

diff -r 5c5f08f6d6e4 -r 4e3fe0b8687b src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 21 19:04:46 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 21 19:28:25 2010 +0100
@@ -14,7 +14,7 @@
   val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
-  val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
+  val add_axioms: (Attrib.binding * string) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
   val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
@@ -164,16 +164,14 @@
   in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos txt)) end;
 
 
-(* axioms *)
+(* old-style axioms *)
 
-fun add_axms f args thy =
-  f (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+val add_axioms = fold (fn (b, ax) => snd o Specification.axiomatization_cmd [] [(b, [ax])]);
 
-val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
-
-fun add_defs ((unchecked, overloaded), args) =
-  add_axms
-    (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
+fun add_defs ((unchecked, overloaded), args) thy =
+  thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded
+    (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
+  |> snd;
 
 
 (* declarations *)
diff -r 5c5f08f6d6e4 -r 4e3fe0b8687b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 21 19:04:46 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 21 19:28:25 2010 +0100
@@ -178,11 +178,9 @@
 
 (* axioms and definitions *)
 
-val named_spec = SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
-
 val _ =
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
-    (Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms));
+    (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
 
 val opt_unchecked_overloaded =
   Scan.optional (P.$$$ "(" |-- P.!!!
@@ -191,7 +189,8 @@
 
 val _ =
   OuterSyntax.command "defs" "define constants" K.thy_decl
-    (opt_unchecked_overloaded -- Scan.repeat1 named_spec
+    (opt_unchecked_overloaded --
+      Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
       >> (Toplevel.theory o IsarCmd.add_defs));
 
 
diff -r 5c5f08f6d6e4 -r 4e3fe0b8687b src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Mar 21 19:04:46 2010 +0100
+++ b/src/Pure/pure_thy.ML	Sun Mar 21 19:28:25 2010 +0100
@@ -33,7 +33,6 @@
   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_axioms_cmd: ((binding * string) * 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 ->
@@ -216,7 +215,6 @@
   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;
-  val add_axioms_cmd         = add_axm Theory.add_axioms;
 end;