diff -r 7a642e5c272c -r 3eb598b044ad src/HOL/TPTP/atp_problem_import.ML
--- 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"),