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;