src/Pure/codegen.ML

         val (s, T) = dest_Const c
       in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
       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])))))))
   in
     fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty