# HG changeset patch # User blanchet # Date 1334999749 -7200 # Node ID 9460f3f22365a159da4ccfe718f2c86d7664a22f # Parent 8ca67d2b21c2a2f3bae87afbfa6846f939d482bd tried to make SML/NJ happy diff -r 8ca67d2b21c2 -r 9460f3f22365 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Apr 21 11:15:49 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Apr 21 11:15:49 2012 +0200 @@ -202,7 +202,7 @@ (* FUDGE *) [(1.0, (false, ((100, alt_ergo_tff1, "poly_native", liftingN, false), "")))]} -val alt_ergo = (alt_ergoN, K alt_ergo_config) +val alt_ergo = (alt_ergoN, fn () => alt_ergo_config) (* E *) @@ -318,7 +318,7 @@ [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), heuristic)))] end} -val e = (eN, K e_config) +val e = (eN, fn () => e_config) (* LEO-II *) @@ -346,7 +346,7 @@ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} -val leo2 = (leo2N, K leo2_config) +val leo2 = (leo2N, fn () => leo2_config) (* Satallax *) @@ -368,7 +368,7 @@ (* FUDGE *) K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]} -val satallax = (satallaxN, K satallax_config) +val satallax = (satallaxN, fn () => satallax_config) (* SPASS *) @@ -405,7 +405,7 @@ (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} -val spass_old = (spass_oldN, K spass_old_config) +val spass_old = (spass_oldN, fn () => spass_old_config) val spass_new_H1SOS = "-Heuristic=1 -SOS" val spass_new_H2 = "-Heuristic=2" @@ -435,7 +435,7 @@ (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)))]} -val spass_new = (spass_newN, K spass_new_config) +val spass_new = (spass_newN, fn () => spass_new_config) val spass = (spassN, fn () => if is_new_spass_version () then spass_new_config @@ -486,7 +486,7 @@ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} -val vampire = (vampireN, K vampire_config) +val vampire = (vampireN, fn () => vampire_config) (* Z3 with TPTP syntax *) @@ -509,7 +509,7 @@ (0.125, (false, ((62, z3_tff0, "mono_native", combsN, false), ""))), (0.125, (false, ((31, z3_tff0, "mono_native", combsN, false), "")))]} -val z3_tptp = (z3_tptpN, K z3_tptp_config) +val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) (* Not really a prover: Experimental Polymorphic TFF and THF output *) @@ -529,7 +529,7 @@ val dummy_thf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice) val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher" -val dummy_thf = (dummy_thfN, K dummy_thf_config) +val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) (* Remote ATP invocation via SystemOnTPTP *)