--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 24 08:19:56 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 24 08:19:57 2014 +0200
@@ -608,16 +608,17 @@
SOME s => (SOME Type_Class_Polymorphic, s)
| NONE =>
(case try (unprefix "poly_") s of
- (* It's still unclear whether all TFF1 implementations will support type signatures such as
- "!>[A : $tType] : $o", with phantom type variables. *)
SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
| NONE =>
- (case try (unprefix "raw_mono_") s of
- SOME s => (SOME Raw_Monomorphic, s)
+ (case try (unprefix "ml_poly_") s of
+ SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s)
| NONE =>
- (case try (unprefix "mono_") s of
- SOME s => (SOME Mangled_Monomorphic, s)
- | NONE => (NONE, s)))))
+ (case try (unprefix "raw_mono_") s of
+ SOME s => (SOME Raw_Monomorphic, s)
+ | NONE =>
+ (case try (unprefix "mono_") s of
+ SOME s => (SOME Mangled_Monomorphic, s)
+ | NONE => (NONE, s))))))
||> (fn s =>
(case try_unsuffixes queries s of
SOME s =>
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 24 08:19:56 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 24 08:19:57 2014 +0200
@@ -46,6 +46,7 @@
val agsyholN : string
val alt_ergoN : string
val dummy_thfN : string
+ val dummy_thf_mlN : string
val eN : string
val e_malesN : string
val e_parN : string
@@ -100,6 +101,7 @@
val agsyholN = "agsyhol"
val alt_ergoN = "alt_ergo"
val dummy_thfN = "dummy_thf" (* for experiments *)
+val dummy_thf_mlN = "dummy_thf_ml" (* for experiments *)
val eN = "e"
val e_malesN = "e_males"
val e_parN = "e_par"
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 24 08:19:56 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 24 08:19:57 2014 +0200
@@ -628,9 +628,13 @@
best_max_new_mono_instances = default_max_new_mono_instances}
val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
+
val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
+val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false
+val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config)
+
val spass_pirate_format = DFG Polymorphic
val remote_spass_pirate_config : atp_config =
{exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
@@ -797,9 +801,9 @@
val atps =
[agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
- z3_tptp, zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
- remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
- remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
+ z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
+ remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
+ remote_snark, remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
val _ = Theory.setup (fold add_atp atps)