# HG changeset patch # User blanchet # Date 1314309321 -7200 # Node ID 97ec9abd3253df2e590e3d9370d10c280e8a3dea # Parent c537d5e5a3656bde7b9037de8ebe8aca9ab41269 make sure that if slicing is disabled, a non-SOS slice is chosen diff -r c537d5e5a365 -r 97ec9abd3253 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 25 23:54:57 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Aug 25 23:55:21 2011 +0200 @@ -335,12 +335,12 @@ (* FUDGE *) (if is_old_vampire_version () then [(0.333, (false, (150, FOF, "poly_guards", sosN))), - (0.334, (true, (50, FOF, "mono_guards?", no_sosN))), - (0.333, (false, (500, FOF, "mono_tags?", sosN)))] + (0.333, (false, (500, FOF, "mono_tags?", sosN))), + (0.334, (true, (50, FOF, "mono_guards?", no_sosN)))] else [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))), - (0.334, (true, (50, TFF Implicit, "simple", no_sosN))), - (0.333, (false, (500, TFF Implicit, "simple", sosN)))]) + (0.333, (false, (500, TFF Implicit, "simple", sosN))), + (0.334, (true, (50, TFF Implicit, "simple", no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}