--- 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
--- 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*)
--- 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
--- 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
--- 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)
--- 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])))))))
--- 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
--- 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);
--- 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;
--- 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