# HG changeset patch
# User wenzelm
# Date 1224768485 -7200
# Node ID fb68c07670045ae03762377cb40b25de5a8ad237
# Parent  08a77c495dc181b026b30ac4bf563feb41c252e0
renamed get_axiom_i to axiom, removed obsolete get_axiom;
reduced pervasive names;

diff -r 08a77c495dc1 -r fb68c0767004 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 23 15:28:01 2008 +0200
+++ b/src/Pure/thm.ML	Thu Oct 23 15:28:05 2008 +0200
@@ -71,12 +71,6 @@
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
   val strip_shyps: thm -> thm
-  val get_axiom_i: theory -> string -> thm
-  val get_axiom: theory -> xstring -> thm
-  val def_name: string -> string
-  val def_name_optional: string -> string -> string
-  val get_def: theory -> xstring -> thm
-  val axioms_of: theory -> (string * thm) list
 
   (*meta rules*)
   val assume: cterm -> thm
@@ -139,6 +133,11 @@
   val maxidx_thm: thm -> int -> int
   val hyps_of: thm -> term list
   val full_prop_of: thm -> term
+  val axiom: theory -> string -> thm
+  val def_name: string -> string
+  val def_name_optional: string -> string -> string
+  val get_def: theory -> xstring -> thm
+  val axioms_of: theory -> (string * thm) list
   val get_name: thm -> string
   val put_name: string -> thm -> thm
   val get_tags: thm -> Properties.T
@@ -542,8 +541,7 @@
 
 (** Axioms **)
 
-(*look up the named axiom in the theory or its ancestors*)
-fun get_axiom_i theory name =
+fun axiom theory name =
   let
     fun get_ax thy =
       Symtab.lookup (Theory.axiom_table thy) name
@@ -562,20 +560,17 @@
     | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
   end;
 
-fun get_axiom thy =
-  get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy);
-
 fun def_name c = c ^ "_def";
 
 fun def_name_optional c "" = def_name c
   | def_name_optional _ name = name;
 
-fun get_def thy = get_axiom thy o def_name;
+fun get_def thy = axiom thy o NameSpace.intern (Theory.axiom_space thy) o def_name;
 
 
 (*return additional axioms of this theory node*)
 fun axioms_of thy =
-  map (fn s => (s, get_axiom_i thy s)) (Symtab.keys (Theory.axiom_table thy));
+  map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));
 
 
 (* official name and additional tags *)