# HG changeset patch
# User wenzelm
# Date 1224768481 -7200
# Node ID 08a77c495dc181b026b30ac4bf563feb41c252e0
# Parent  d746a8c12c43f8afbc466a07626f167925e217f1
renamed Thm.get_axiom_i to Thm.axiom;

diff -r d746a8c12c43 -r 08a77c495dc1 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 23 14:22:16 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 23 15:28:01 2008 +0200
@@ -594,7 +594,7 @@
   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
-  @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
+  @{index_ML Thm.axiom: "theory -> string -> thm"} \\
   @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
   -> (string * ('a -> thm)) * theory"} \\
   \end{mldecls}
@@ -648,7 +648,7 @@
   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
   refer to the instantiated versions.
 
-  \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
+  \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
   axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
 
   \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
diff -r d746a8c12c43 -r 08a77c495dc1 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -87,7 +87,7 @@
               Sign.declare_const [Markup.property_internal] ((Name.binding cname, cT), NoSyn) thy
             val cdef = cname ^ "_def"
             val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
-            val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
+            val ax = Thm.axiom thy'' (Sign.full_name thy'' cdef)
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
       | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
           (*Universal quant: insert a free variable into body and continue*)
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/Isar/class.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -497,7 +497,7 @@
     val ty' = Term.fastype_of dict_def;
     val ty'' = Type.strip_sorts ty';
     val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
-    fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy);
+    fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   in
     thy'
     |> Sign.declare_const pos ((Name.binding c, ty''), mx) |> snd
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -356,7 +356,7 @@
     val is_def =
       (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
          (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
-           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
+           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.axiom thy) name)
        | _ => false) handle TERM _ => false;
   in
     (ExtractionData.put (if is_def then
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -56,7 +56,7 @@
           in thm_of_atom thm Ts end
 
       | thm_of _ _ (PAxm (name, _, SOME Ts)) =
-          thm_of_atom (get_axiom_i thy name) Ts
+          thm_of_atom (Thm.axiom thy name) Ts
 
       | thm_of _ Hs (PBound i) = List.nth (Hs, i)
 
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/codegen.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -508,7 +508,7 @@
       end handle TERM _ => NONE;
     fun add_def thyname (name, t) = (case dest t of
         NONE => I
-      | SOME _ => (case dest (prep_def (Thm.get_axiom_i thy name)) of
+      | SOME _ => (case dest (prep_def (Thm.axiom thy name)) of
           NONE => I
         | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, [])
             (cons (T, (thyname, split_last (rename_terms (args @ [rhs])))))))
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/conjunction.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -70,7 +70,7 @@
 val A_B = read_prop "A && B";
 
 val conjunction_def =
-  Thm.unvarify (Thm.get_axiom (Context.the_theory (Context.the_thread_data ())) "conjunction_def");
+  Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
 
 fun conjunctionD which =
   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/drule.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -681,10 +681,10 @@
 
 local
   val A = certify (Free ("A", propT));
-  val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ()));
-  val prop_def = get_axiom "prop_def";
-  val term_def = get_axiom "term_def";
-  val sort_constraint_def = get_axiom "sort_constraint_def";
+  val axiom = Thm.unvarify o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
+  val prop_def = axiom "Pure.prop_def";
+  val term_def = axiom "Pure.term_def";
+  val sort_constraint_def = axiom "Pure.sort_constraint_def";
   val C = Thm.lhs_of sort_constraint_def;
   val T = Thm.dest_arg C;
   val CA = mk_implies (C, A);
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/more_thm.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -281,7 +281,7 @@
   let
     val name' = if name = "" then "axiom_" ^ serial_string () else name;
     val thy' = thy |> Theory.add_axioms_i [(name', prop)];
-    val axm = unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
+    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' name'));
   in (axm, thy') end;
 
 fun add_def unchecked overloaded (name, prop) thy =
@@ -293,7 +293,7 @@
 
     val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
     val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
-    val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
+    val axm' = Thm.axiom thy' (Sign.full_name thy' name);
     val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   in (thm, thy') end;
 
diff -r d746a8c12c43 -r 08a77c495dc1 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/pure_thy.ML	Thu Oct 23 15:28:01 2008 +0200
@@ -205,7 +205,7 @@
 (* store axioms as theorems *)
 
 local
-  fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name);
+  fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_name thy name);
   fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
   fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
     let