moved Thm.def_name(_optional) to more_thm.ML;
authorwenzelm
Sat Mar 07 22:04:59 2009 +0100 (2009-03-07)
changeset 30342d32daa6aba3c
parent 30341 78d08e2d01b9
child 30343 79f022df8527
moved Thm.def_name(_optional) to more_thm.ML;
moved old-style Thm.get_def to Drule.get_def;
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/drule.ML	Sat Mar 07 21:57:36 2009 +0100
     1.2 +++ b/src/Pure/drule.ML	Sat Mar 07 22:04:59 2009 +0100
     1.3 @@ -77,6 +77,7 @@
     1.4    val beta_conv: cterm -> cterm -> cterm
     1.5    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
     1.6    val flexflex_unique: thm -> thm
     1.7 +  val get_def: theory -> xstring -> thm
     1.8    val store_thm: bstring -> thm -> thm
     1.9    val store_standard_thm: bstring -> thm -> thm
    1.10    val store_thm_open: bstring -> thm -> thm
    1.11 @@ -459,6 +460,8 @@
    1.12  
    1.13  val read_prop = certify o SimpleSyntax.read_prop;
    1.14  
    1.15 +fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
    1.16 +
    1.17  fun store_thm name th =
    1.18    Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
    1.19  
     2.1 --- a/src/Pure/more_thm.ML	Sat Mar 07 21:57:36 2009 +0100
     2.2 +++ b/src/Pure/more_thm.ML	Sat Mar 07 22:04:59 2009 +0100
     2.3 @@ -55,6 +55,8 @@
     2.4    val position_of: thm -> Position.T
     2.5    val default_position: Position.T -> thm -> thm
     2.6    val default_position_of: thm -> thm -> thm
     2.7 +  val def_name: string -> string
     2.8 +  val def_name_optional: string -> string -> string
     2.9    val has_name_hint: thm -> bool
    2.10    val get_name_hint: thm -> string
    2.11    val put_name_hint: string -> thm -> thm
    2.12 @@ -278,6 +280,8 @@
    2.13  
    2.14  (** specification primitives **)
    2.15  
    2.16 +(* rules *)
    2.17 +
    2.18  fun add_axiom (b, prop) thy =
    2.19    let
    2.20      val b' = if Binding.is_empty b
    2.21 @@ -342,6 +346,14 @@
    2.22  val default_position_of = default_position o position_of;
    2.23  
    2.24  
    2.25 +(* def_name *)
    2.26 +
    2.27 +fun def_name c = c ^ "_def";
    2.28 +
    2.29 +fun def_name_optional c "" = def_name c
    2.30 +  | def_name_optional _ name = name;
    2.31 +
    2.32 +
    2.33  (* unofficial theorem names *)
    2.34  
    2.35  fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
     3.1 --- a/src/Pure/thm.ML	Sat Mar 07 21:57:36 2009 +0100
     3.2 +++ b/src/Pure/thm.ML	Sat Mar 07 22:04:59 2009 +0100
     3.3 @@ -128,9 +128,6 @@
     3.4    val hyps_of: thm -> term list
     3.5    val full_prop_of: thm -> term
     3.6    val axiom: theory -> string -> thm
     3.7 -  val def_name: string -> string
     3.8 -  val def_name_optional: string -> string -> string
     3.9 -  val get_def: theory -> xstring -> thm
    3.10    val axioms_of: theory -> (string * thm) list
    3.11    val get_name: thm -> string
    3.12    val put_name: string -> thm -> thm
    3.13 @@ -558,14 +555,6 @@
    3.14      | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
    3.15    end;
    3.16  
    3.17 -fun def_name c = c ^ "_def";
    3.18 -
    3.19 -fun def_name_optional c "" = def_name c
    3.20 -  | def_name_optional _ name = name;
    3.21 -
    3.22 -fun get_def thy = axiom thy o NameSpace.intern (Theory.axiom_space thy) o def_name;
    3.23 -
    3.24 -
    3.25  (*return additional axioms of this theory node*)
    3.26  fun axioms_of thy =
    3.27    map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));