# HG changeset patch
# User blanchet
# Date 1362481198 -3600
# Node ID 6c06b8de72f919c469843de703eb04f31a6442b6
# Parent  6bac04a6a197195c3a8c301e808de49a50d55986
polymorphic SPASS is also SPASS

diff -r 6bac04a6a197 -r 6c06b8de72f9 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 05 09:47:15 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 05 11:59:58 2013 +0100
@@ -766,11 +766,10 @@
 fun effective_term_order ctxt atp =
   let val ord = Config.get ctxt term_order in
     if ord = smartN then
-      if atp = spassN then
-        {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
-      else
-        {is_lpo = false, gen_weights = false, gen_prec = false,
+      let val is_spass = (atp = spassN orelse atp = spass_polyN) in
+        {is_lpo = false, gen_weights = is_spass, gen_prec = is_spass,
          gen_simp = false}
+      end
     else
       let val is_lpo = String.isSubstring lpoN ord in
         {is_lpo = is_lpo,