--- a/src/Pure/Proof/extraction.ML Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Aug 14 16:52:46 2008 +0200
@@ -356,7 +356,7 @@
val is_def =
(case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
(Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
- andalso (PureThy.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
+ andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
| _ => false) handle TERM _ => false;
in
(ExtractionData.put (if is_def then