renamed get_axiom_i to axiom, removed obsolete get_axiom;
authorwenzelm
Thu Oct 23 15:28:05 2008 +0200 (2008-10-23)
changeset 28675fb68c0767004
parent 28674 08a77c495dc1
child 28676 78688a5fafc2
renamed get_axiom_i to axiom, removed obsolete get_axiom;
reduced pervasive names;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Oct 23 15:28:01 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Oct 23 15:28:05 2008 +0200
     1.3 @@ -71,12 +71,6 @@
     1.4    val weaken_sorts: sort list -> cterm -> cterm
     1.5    val extra_shyps: thm -> sort list
     1.6    val strip_shyps: thm -> thm
     1.7 -  val get_axiom_i: theory -> string -> thm
     1.8 -  val get_axiom: theory -> xstring -> thm
     1.9 -  val def_name: string -> string
    1.10 -  val def_name_optional: string -> string -> string
    1.11 -  val get_def: theory -> xstring -> thm
    1.12 -  val axioms_of: theory -> (string * thm) list
    1.13  
    1.14    (*meta rules*)
    1.15    val assume: cterm -> thm
    1.16 @@ -139,6 +133,11 @@
    1.17    val maxidx_thm: thm -> int -> int
    1.18    val hyps_of: thm -> term list
    1.19    val full_prop_of: thm -> term
    1.20 +  val axiom: theory -> string -> thm
    1.21 +  val def_name: string -> string
    1.22 +  val def_name_optional: string -> string -> string
    1.23 +  val get_def: theory -> xstring -> thm
    1.24 +  val axioms_of: theory -> (string * thm) list
    1.25    val get_name: thm -> string
    1.26    val put_name: string -> thm -> thm
    1.27    val get_tags: thm -> Properties.T
    1.28 @@ -542,8 +541,7 @@
    1.29  
    1.30  (** Axioms **)
    1.31  
    1.32 -(*look up the named axiom in the theory or its ancestors*)
    1.33 -fun get_axiom_i theory name =
    1.34 +fun axiom theory name =
    1.35    let
    1.36      fun get_ax thy =
    1.37        Symtab.lookup (Theory.axiom_table thy) name
    1.38 @@ -562,20 +560,17 @@
    1.39      | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
    1.40    end;
    1.41  
    1.42 -fun get_axiom thy =
    1.43 -  get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy);
    1.44 -
    1.45  fun def_name c = c ^ "_def";
    1.46  
    1.47  fun def_name_optional c "" = def_name c
    1.48    | def_name_optional _ name = name;
    1.49  
    1.50 -fun get_def thy = get_axiom thy o def_name;
    1.51 +fun get_def thy = axiom thy o NameSpace.intern (Theory.axiom_space thy) o def_name;
    1.52  
    1.53  
    1.54  (*return additional axioms of this theory node*)
    1.55  fun axioms_of thy =
    1.56 -  map (fn s => (s, get_axiom_i thy s)) (Symtab.keys (Theory.axiom_table thy));
    1.57 +  map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));
    1.58  
    1.59  
    1.60  (* official name and additional tags *)