# HG changeset patch
# User blanchet
# Date 1335558987 -7200
# Node ID 1e8eb643540d755259c28a54a19d6bb052786746
# Parent  9579464d00f93cda0841a2756dbe7094d2f0dd76
add extensionality to first-order provers

diff -r 9579464d00f9 -r 1e8eb643540d src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:36:27 2012 +0200
@@ -140,7 +140,8 @@
         ("overlord", if overlord then "true" else "false"),
         ("provers", prover),
         ("timeout", string_of_int timeout)] @ override_params)
-      {add = [], del = [], only = true}
+      {add = [(Facts.named (Thm.derivation_name ext), [])],
+       del = [], only = true}
 
 fun sledgehammer_tac ctxt timeout i =
   let
@@ -207,8 +208,8 @@
       read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
   in
-    (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+     can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
      can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
     |> print_szs_from_success conjs
   end