minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
authorwenzelm
Sun Mar 21 19:28:25 2010 +0100 (2010-03-21 ago)
changeset 358524e3fe0b8687b
parent 35851 5c5f08f6d6e4
child 35853 f2126d4d0486
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 21 19:04:46 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 21 19:28:25 2010 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     1.5    val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     1.6    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
     1.7 -  val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
     1.8 +  val add_axioms: (Attrib.binding * string) list -> theory -> theory
     1.9    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    1.10    val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
    1.11    val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
    1.12 @@ -164,16 +164,14 @@
    1.13    in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos txt)) end;
    1.14  
    1.15  
    1.16 -(* axioms *)
    1.17 +(* old-style axioms *)
    1.18  
    1.19 -fun add_axms f args thy =
    1.20 -  f (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) thy;
    1.21 +val add_axioms = fold (fn (b, ax) => snd o Specification.axiomatization_cmd [] [(b, [ax])]);
    1.22  
    1.23 -val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
    1.24 -
    1.25 -fun add_defs ((unchecked, overloaded), args) =
    1.26 -  add_axms
    1.27 -    (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
    1.28 +fun add_defs ((unchecked, overloaded), args) thy =
    1.29 +  thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded
    1.30 +    (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
    1.31 +  |> snd;
    1.32  
    1.33  
    1.34  (* declarations *)
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 21 19:04:46 2010 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 21 19:28:25 2010 +0100
     2.3 @@ -178,11 +178,9 @@
     2.4  
     2.5  (* axioms and definitions *)
     2.6  
     2.7 -val named_spec = SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
     2.8 -
     2.9  val _ =
    2.10    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
    2.11 -    (Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms));
    2.12 +    (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
    2.13  
    2.14  val opt_unchecked_overloaded =
    2.15    Scan.optional (P.$$$ "(" |-- P.!!!
    2.16 @@ -191,7 +189,8 @@
    2.17  
    2.18  val _ =
    2.19    OuterSyntax.command "defs" "define constants" K.thy_decl
    2.20 -    (opt_unchecked_overloaded -- Scan.repeat1 named_spec
    2.21 +    (opt_unchecked_overloaded --
    2.22 +      Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
    2.23        >> (Toplevel.theory o IsarCmd.add_defs));
    2.24  
    2.25  
     3.1 --- a/src/Pure/pure_thy.ML	Sun Mar 21 19:04:46 2010 +0100
     3.2 +++ b/src/Pure/pure_thy.ML	Sun Mar 21 19:28:25 2010 +0100
     3.3 @@ -33,7 +33,6 @@
     3.4    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
     3.5      -> theory -> (string * thm list) list * theory
     3.6    val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
     3.7 -  val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
     3.8    val add_defs: bool -> ((binding * term) * attribute list) list ->
     3.9      theory -> thm list * theory
    3.10    val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
    3.11 @@ -216,7 +215,6 @@
    3.12    val add_axioms             = add_axm Theory.add_axioms_i;
    3.13    val add_defs_cmd           = add_axm o Theory.add_defs false;
    3.14    val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
    3.15 -  val add_axioms_cmd         = add_axm Theory.add_axioms;
    3.16  end;
    3.17  
    3.18