src/Pure/Proof/extraction.ML
changeset 27865 27a8ad9612a3
parent 27691 ce171cbd4b93
child 28370 37f56e6e702d
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Aug 14 11:55:05 2008 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Aug 14 16:52:46 2008 +0200
     1.3 @@ -356,7 +356,7 @@
     1.4      val is_def =
     1.5        (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
     1.6           (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
     1.7 -           andalso (PureThy.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
     1.8 +           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
     1.9         | _ => false) handle TERM _ => false;
    1.10    in
    1.11      (ExtractionData.put (if is_def then