# HG changeset patch
# User blanchet
# Date 1337698767 -7200
# Node ID d2bdd85ee23c6639f969cacc50b1fb34c9da6725
# Parent  2a420750248bc107aecd277c6c7c420803702009
compile

diff -r 2a420750248b -r d2bdd85ee23c src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Tue May 22 16:59:27 2012 +0200
@@ -75,7 +75,7 @@
   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.extensionalize_term ctxt
+    val defs = defs |> map (ATP_Util.abs_extensionalize_term ctxt
                             #> aptrueprop (open_form I))
     val state = Proof.init ctxt
     val params =