# HG changeset patch
# User blanchet
# Date 1337185011 -7200
# Node ID 406d1df3787e944b96b2195ac20485eaf1daf912
# Parent  c06aa331bb76232c57672ef415780e31746ba1b3
minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)

diff -r c06aa331bb76 -r 406d1df3787e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 16 18:16:51 2012 +0200
@@ -417,10 +417,10 @@
       (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
       (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
       (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
-      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0))),
       (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
       (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),
-      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS)))]}
+      (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
+      (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))]}
 
 val spass_new = (spass_newN, fn () => spass_new_config)