Adapted to new naming scheme for definitions.

--- a/src/Pure/Proof/extraction.ML	Thu May 10 15:50:28 2007 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu May 10 15:50:56 2007 +0200
@@ -360,7 +360,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 can (Thm.get_axiom_i thy) name
+           andalso (PureThy.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
        | _ => false) handle TERM _ => false;
   in
     (ExtractionData.put (if is_def then