# HG changeset patch
# User traytel
# Date 1578413574 -3600
# Node ID 15c6f253b9f345731b3b85997367900e589805b3
# Parent  c71a44893645489c56017613828474c0cd75fde4# Parent  475b2260b9c4ab01cd259984787bee5c6351c333
merged

diff -r c71a44893645 -r 15c6f253b9f3 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 07 14:58:01 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 07 17:12:54 2020 +0100
@@ -45,7 +45,6 @@
   val spass_H2NuVS0 : string
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
-  val spass_extra_options : string Config.T
   val is_vampire_noncommercial_license_accepted : unit -> bool option
   val remote_atp : string -> string -> string list -> (string * string) list ->
     (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
@@ -437,9 +436,6 @@
 val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
 val spass_H2SOS = "-Heuristic=2 -SOS"
 
-val spass_extra_options =
-  Attrib.setup_config_string \<^binding>\<open>atp_spass_extra_options\<close> (K "")
-
 val spass_config : atp_config =
   {exec = K (["SPASS_HOME"], ["SPASS"]),
    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ =>
@@ -466,10 +462,7 @@
       (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
       (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
       (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
-      (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
-     |> (case Config.get ctxt spass_extra_options of
-           "" => I
-         | opts => map (apsnd (apsnd (K opts)))),
+      (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}