# HG changeset patch
# User blanchet
# Date 1308669459 -7200
# Node ID 13eefebbc4cbea6f4950891466820c047785368b
# Parent  bdb11c68f1421f81614f0b7e260835a699ef71bf
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity

diff -r bdb11c68f142 -r 13eefebbc4cb src/HOL/ex/atp_export.ML
--- a/src/HOL/ex/atp_export.ML	Tue Jun 21 17:17:39 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Tue Jun 21 17:17:39 2011 +0200
@@ -8,6 +8,8 @@
 
 signature ATP_EXPORT =
 sig
+  val theorems_mentioned_in_proof_term :
+    string list option -> thm -> string list
   val generate_tptp_graph_file_for_theory :
     Proof.context -> theory -> string -> unit
   val generate_tptp_inference_file_for_theory :
@@ -110,7 +112,7 @@
       facts0 |> map (fn ((_, loc), th) =>
                         ((Thm.get_name_hint th, loc), prop_of th))
     val (atp_problem, _, _, _, _, _, _) =
-      prepare_atp_problem ctxt format Axiom Axiom type_sys false false true []
+      prepare_atp_problem ctxt format Axiom Axiom type_sys true false true []
                           @{prop False} facts
     val all_names = facts0 |> map (Thm.get_name_hint o snd)
     val infers =