can (Thm.get_axiom_i thy) name;
removed duplicate code;

--- a/src/Pure/Proof/extraction.ML	Thu Jun 09 12:03:35 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Jun 09 12:03:36 2005 +0200
@@ -376,13 +376,8 @@
     val is_def =
       (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
          (Const _, ts) => forall is_Var ts andalso null (duplicates ts)
-           andalso exists (fn thy =>
-               isSome (Symtab.lookup (#axioms (rep_theory thy), name)))
-             (thy :: ancestors_of thy)
+           andalso can (Thm.get_axiom_i thy) name
        | _ => false) handle TERM _ => false;
-
-    val name = Thm.name_of_thm thm;
-    val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
   in
     (ExtractionData.put (if is_def then
         {realizes_eqns = realizes_eqns,