--- 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,