src/Pure/Proof/extraction.ML
changeset 28674 08a77c495dc1
parent 28375 c879d88d038a
child 28805 8136e5736808
--- a/src/Pure/Proof/extraction.ML	Thu Oct 23 14:22:16 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Oct 23 15:28:01 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 (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
+           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.axiom thy) name)
        | _ => false) handle TERM _ => false;
   in
     (ExtractionData.put (if is_def then