--- a/src/HOL/TPTP/atp_problem_import.ML Thu May 24 17:46:35 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Thu May 24 18:21:54 2012 +0200
@@ -75,8 +75,13 @@
let
val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
val thy = Proof_Context.theory_of ctxt
- val defs = defs |> map (ATP_Util.abs_extensionalize_term ctxt
- #> aptrueprop (open_form I))
+ val (defs, pseudo_defs) =
+ defs |> map (ATP_Util.abs_extensionalize_term ctxt
+ #> aptrueprop (open_form I))
+ |> List.partition (ATP_Util.is_legitimate_tptp_def
+ o perhaps (try HOLogic.dest_Trueprop)
+ o ATP_Util.unextensionalize_def)
+ val nondefs = pseudo_defs @ nondefs
val state = Proof.init ctxt
val params =
[("card", "1\<emdash>100"),