minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
--- 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 *)
--- 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));
--- 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;