# HG changeset patch
# User blanchet
# Date 1314121761 -7200
# Node ID 61fa3dd485b3d57c771f23ceb7d13fe920311cd6
# Parent  3e0ce0ae102294cc53dd5785efdd80d08fd60d5d
compile

diff -r 3e0ce0ae1022 -r 61fa3dd485b3 src/HOL/TPTP/CASC_Setup.thy
--- a/src/HOL/TPTP/CASC_Setup.thy	Tue Aug 23 19:00:48 2011 +0200
+++ b/src/HOL/TPTP/CASC_Setup.thy	Tue Aug 23 19:49:21 2011 +0200
@@ -119,14 +119,14 @@
    SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
-       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
-       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
+       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "metis"
        (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))