src/Pure/more_thm.ML
changeset 28674 08a77c495dc1
parent 28621 a60164e8fff0
child 28965 1de908189869
     1.1 --- a/src/Pure/more_thm.ML	Thu Oct 23 14:22:16 2008 +0200
     1.2 +++ b/src/Pure/more_thm.ML	Thu Oct 23 15:28:01 2008 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4    let
     1.5      val name' = if name = "" then "axiom_" ^ serial_string () else name;
     1.6      val thy' = thy |> Theory.add_axioms_i [(name', prop)];
     1.7 -    val axm = unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
     1.8 +    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' name'));
     1.9    in (axm, thy') end;
    1.10  
    1.11  fun add_def unchecked overloaded (name, prop) thy =
    1.12 @@ -293,7 +293,7 @@
    1.13  
    1.14      val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
    1.15      val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
    1.16 -    val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
    1.17 +    val axm' = Thm.axiom thy' (Sign.full_name thy' name);
    1.18      val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
    1.19    in (thm, thy') end;
    1.20