# HG changeset patch
# User wenzelm
# Date 1305369611 -7200
# Node ID df2dc94062870494814418a546556962a3eeb64b
# Parent  4e33894aec6dd37ba72e595d37fc654b5556e6ef
just one universal Proof.context -- discontinued claset/clasimpset;

diff -r 4e33894aec6d -r df2dc9406287 src/HOL/ex/CASC_Setup.thy
--- a/src/HOL/ex/CASC_Setup.thy	Sat May 14 11:42:43 2011 +0200
+++ b/src/HOL/ex/CASC_Setup.thy	Sat May 14 12:40:11 2011 +0200
@@ -38,28 +38,28 @@
 *}
 
 ML {*
-fun isabellep_tac ctxt cs ss css max_secs =
+fun isabellep_tac ctxt max_secs =
    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))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac ss))
+   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 cs))
+   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac css
+   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_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 []))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac cs))
+   SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac cs))
+   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
    ORELSE
-   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac css))
+   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
    ORELSE
-   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac css))
+   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
 *}
 
 end