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