src/Pure/codegen.ML

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