polymorphic SPASS is also SPASS
authorblanchet
Tue Mar 05 11:59:58 2013 +0100 (2013-03-05)
changeset 513366c06b8de72f9
parent 51335 6bac04a6a197
child 51337 1012626af0bc
polymorphic SPASS is also SPASS
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 05 09:47:15 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 05 11:59:58 2013 +0100
     1.3 @@ -766,11 +766,10 @@
     1.4  fun effective_term_order ctxt atp =
     1.5    let val ord = Config.get ctxt term_order in
     1.6      if ord = smartN then
     1.7 -      if atp = spassN then
     1.8 -        {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
     1.9 -      else
    1.10 -        {is_lpo = false, gen_weights = false, gen_prec = false,
    1.11 +      let val is_spass = (atp = spassN orelse atp = spass_polyN) in
    1.12 +        {is_lpo = false, gen_weights = is_spass, gen_prec = is_spass,
    1.13           gen_simp = false}
    1.14 +      end
    1.15      else
    1.16        let val is_lpo = String.isSubstring lpoN ord in
    1.17          {is_lpo = is_lpo,