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
1.1 --- a/src/HOL/ex/atp_export.ML Tue Jun 21 17:17:39 2011 +0200
1.2 +++ b/src/HOL/ex/atp_export.ML Tue Jun 21 17:17:39 2011 +0200
1.3 @@ -8,6 +8,8 @@
1.4
1.5 signature ATP_EXPORT =
1.6 sig
1.7 + val theorems_mentioned_in_proof_term :
1.8 + string list option -> thm -> string list
1.9 val generate_tptp_graph_file_for_theory :
1.10 Proof.context -> theory -> string -> unit
1.11 val generate_tptp_inference_file_for_theory :
1.12 @@ -110,7 +112,7 @@
1.13 facts0 |> map (fn ((_, loc), th) =>
1.14 ((Thm.get_name_hint th, loc), prop_of th))
1.15 val (atp_problem, _, _, _, _, _, _) =
1.16 - prepare_atp_problem ctxt format Axiom Axiom type_sys false false true []
1.17 + prepare_atp_problem ctxt format Axiom Axiom type_sys true false true []
1.18 @{prop False} facts
1.19 val all_names = facts0 |> map (Thm.get_name_hint o snd)
1.20 val infers =