# HG changeset patch
# User blanchet
# Date 1301920640 -7200
# Node ID bac7733a13c909648ea1e70b79074057ff96b34b
# Parent  b33d871675bb8a61b4c0544c9614d90418a589be
use the proper contexts/simpsets/etc. in the TPTP proof method

diff -r b33d871675bb -r bac7733a13c9 src/HOL/ex/TPTP.thy
--- a/src/HOL/ex/TPTP.thy	Mon Apr 04 13:41:56 2011 +0200
+++ b/src/HOL/ex/TPTP.thy	Mon Apr 04 14:37:20 2011 +0200
@@ -30,32 +30,34 @@
         | ERROR _ => NONE
   in
     (case result of
-      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
-    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
+      NONE => (warning ("FAILURE: " ^ name); Seq.empty)
+    | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
   end
 *}
 
 ML {*
-fun isabellep_tac max_secs =
-   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
-       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+fun isabellep_tac ctxt cs ss css max_secs =
+   SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
+   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
+       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
+   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac cs))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
-       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css
+       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
+   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
+   SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
+   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
+   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css))
    ORELSE
-   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
+   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css))
 *}
 
 end