renamed Thm.get_axiom_i to Thm.axiom;
authorwenzelm
Thu Oct 23 15:28:01 2008 +0200 (2008-10-23)
changeset 2867408a77c495dc1
parent 28673 d746a8c12c43
child 28675 fb68c0767004
renamed Thm.get_axiom_i to Thm.axiom;
doc-src/IsarImplementation/Thy/logic.thy
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/class.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proofchecker.ML
src/Pure/codegen.ML
src/Pure/conjunction.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Pure/pure_thy.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 23 14:22:16 2008 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 23 15:28:01 2008 +0200
     1.3 @@ -594,7 +594,7 @@
     1.4    @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
     1.5    @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
     1.6    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
     1.7 -  @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
     1.8 +  @{index_ML Thm.axiom: "theory -> string -> thm"} \\
     1.9    @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
    1.10    -> (string * ('a -> thm)) * theory"} \\
    1.11    \end{mldecls}
    1.12 @@ -648,7 +648,7 @@
    1.13    term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
    1.14    refer to the instantiated versions.
    1.15  
    1.16 -  \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
    1.17 +  \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
    1.18    axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    1.19  
    1.20    \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Oct 23 14:22:16 2008 +0200
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 23 15:28:01 2008 +0200
     2.3 @@ -87,7 +87,7 @@
     2.4                Sign.declare_const [Markup.property_internal] ((Name.binding cname, cT), NoSyn) thy
     2.5              val cdef = cname ^ "_def"
     2.6              val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
     2.7 -            val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
     2.8 +            val ax = Thm.axiom thy'' (Sign.full_name thy'' cdef)
     2.9            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
    2.10        | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
    2.11            (*Universal quant: insert a free variable into body and continue*)
     3.1 --- a/src/Pure/Isar/class.ML	Thu Oct 23 14:22:16 2008 +0200
     3.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 23 15:28:01 2008 +0200
     3.3 @@ -497,7 +497,7 @@
     3.4      val ty' = Term.fastype_of dict_def;
     3.5      val ty'' = Type.strip_sorts ty';
     3.6      val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
     3.7 -    fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy);
     3.8 +    fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
     3.9    in
    3.10      thy'
    3.11      |> Sign.declare_const pos ((Name.binding c, ty''), mx) |> snd
     4.1 --- a/src/Pure/Proof/extraction.ML	Thu Oct 23 14:22:16 2008 +0200
     4.2 +++ b/src/Pure/Proof/extraction.ML	Thu Oct 23 15:28:01 2008 +0200
     4.3 @@ -356,7 +356,7 @@
     4.4      val is_def =
     4.5        (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
     4.6           (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
     4.7 -           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
     4.8 +           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.axiom thy) name)
     4.9         | _ => false) handle TERM _ => false;
    4.10    in
    4.11      (ExtractionData.put (if is_def then
     5.1 --- a/src/Pure/Proof/proofchecker.ML	Thu Oct 23 14:22:16 2008 +0200
     5.2 +++ b/src/Pure/Proof/proofchecker.ML	Thu Oct 23 15:28:01 2008 +0200
     5.3 @@ -56,7 +56,7 @@
     5.4            in thm_of_atom thm Ts end
     5.5  
     5.6        | thm_of _ _ (PAxm (name, _, SOME Ts)) =
     5.7 -          thm_of_atom (get_axiom_i thy name) Ts
     5.8 +          thm_of_atom (Thm.axiom thy name) Ts
     5.9  
    5.10        | thm_of _ Hs (PBound i) = List.nth (Hs, i)
    5.11  
     6.1 --- a/src/Pure/codegen.ML	Thu Oct 23 14:22:16 2008 +0200
     6.2 +++ b/src/Pure/codegen.ML	Thu Oct 23 15:28:01 2008 +0200
     6.3 @@ -508,7 +508,7 @@
     6.4        end handle TERM _ => NONE;
     6.5      fun add_def thyname (name, t) = (case dest t of
     6.6          NONE => I
     6.7 -      | SOME _ => (case dest (prep_def (Thm.get_axiom_i thy name)) of
     6.8 +      | SOME _ => (case dest (prep_def (Thm.axiom thy name)) of
     6.9            NONE => I
    6.10          | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, [])
    6.11              (cons (T, (thyname, split_last (rename_terms (args @ [rhs])))))))
     7.1 --- a/src/Pure/conjunction.ML	Thu Oct 23 14:22:16 2008 +0200
     7.2 +++ b/src/Pure/conjunction.ML	Thu Oct 23 15:28:01 2008 +0200
     7.3 @@ -70,7 +70,7 @@
     7.4  val A_B = read_prop "A && B";
     7.5  
     7.6  val conjunction_def =
     7.7 -  Thm.unvarify (Thm.get_axiom (Context.the_theory (Context.the_thread_data ())) "conjunction_def");
     7.8 +  Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
     7.9  
    7.10  fun conjunctionD which =
    7.11    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
     8.1 --- a/src/Pure/drule.ML	Thu Oct 23 14:22:16 2008 +0200
     8.2 +++ b/src/Pure/drule.ML	Thu Oct 23 15:28:01 2008 +0200
     8.3 @@ -681,10 +681,10 @@
     8.4  
     8.5  local
     8.6    val A = certify (Free ("A", propT));
     8.7 -  val get_axiom = Thm.unvarify o Thm.get_axiom (Context.the_theory (Context.the_thread_data ()));
     8.8 -  val prop_def = get_axiom "prop_def";
     8.9 -  val term_def = get_axiom "term_def";
    8.10 -  val sort_constraint_def = get_axiom "sort_constraint_def";
    8.11 +  val axiom = Thm.unvarify o Thm.axiom (Context.the_theory (Context.the_thread_data ()));
    8.12 +  val prop_def = axiom "Pure.prop_def";
    8.13 +  val term_def = axiom "Pure.term_def";
    8.14 +  val sort_constraint_def = axiom "Pure.sort_constraint_def";
    8.15    val C = Thm.lhs_of sort_constraint_def;
    8.16    val T = Thm.dest_arg C;
    8.17    val CA = mk_implies (C, A);
     9.1 --- a/src/Pure/more_thm.ML	Thu Oct 23 14:22:16 2008 +0200
     9.2 +++ b/src/Pure/more_thm.ML	Thu Oct 23 15:28:01 2008 +0200
     9.3 @@ -281,7 +281,7 @@
     9.4    let
     9.5      val name' = if name = "" then "axiom_" ^ serial_string () else name;
     9.6      val thy' = thy |> Theory.add_axioms_i [(name', prop)];
     9.7 -    val axm = unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
     9.8 +    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' name'));
     9.9    in (axm, thy') end;
    9.10  
    9.11  fun add_def unchecked overloaded (name, prop) thy =
    9.12 @@ -293,7 +293,7 @@
    9.13  
    9.14      val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
    9.15      val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
    9.16 -    val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
    9.17 +    val axm' = Thm.axiom thy' (Sign.full_name thy' name);
    9.18      val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
    9.19    in (thm, thy') end;
    9.20  
    10.1 --- a/src/Pure/pure_thy.ML	Thu Oct 23 14:22:16 2008 +0200
    10.2 +++ b/src/Pure/pure_thy.ML	Thu Oct 23 15:28:01 2008 +0200
    10.3 @@ -205,7 +205,7 @@
    10.4  (* store axioms as theorems *)
    10.5  
    10.6  local
    10.7 -  fun get_ax thy (name, _) = Thm.get_axiom_i thy (Sign.full_name thy name);
    10.8 +  fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_name thy name);
    10.9    fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
   10.10    fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
   10.11      let