# HG changeset patch
# User wenzelm
# Date 1118311416 -7200
# Node ID 40c5a4d0b3ccbf40bdec3b122ce5d22d63ebe45b
# Parent  7504fe04170fd94b824af7e13817821272f7a2e3
can (Thm.get_axiom_i thy) name;
removed duplicate code;

diff -r 7504fe04170f -r 40c5a4d0b3cc src/Pure/Proof/extraction.ML
--- 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,