--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jul 29 23:39:35 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 00:50:41 2014 +0200
@@ -50,7 +50,7 @@
ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
int Symtab.table -> string atp_proof -> (term, string) atp_step list
val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list
- val infer_formula_types : Proof.context -> term list -> term list
+ val infer_formulas_types : Proof.context -> term list -> term list
val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list ->
(term, string) atp_step list
@@ -197,7 +197,6 @@
val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
val vampire_skolem_prefix = "sK"
-
fun var_index_of_textual textual = if textual then 0 else 1
fun quantify_over_var textual quant_of var_s var_T t =
@@ -380,7 +379,7 @@
val term_ts =
map (do_term [] NONE) us
(* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse
- order, which is incompatible with the new Metis skolemizer. *)
+ order, which is incompatible with "metis"'s new skolemizer. *)
|> exists (fn pre => String.isPrefix pre s)
[spass_skolem_prefix, vampire_skolem_prefix] ? rev
val ts = term_ts @ extra_ts
@@ -538,9 +537,9 @@
else
s
-fun set_var_index j = map_aterms (fn Var ((s, _), T) => Var ((s, j), T) | t => t)
+fun set_var_index j = map_aterms (fn Var ((s, 0), T) => Var ((s, j), T) | t => t)
-fun infer_formula_types ctxt =
+fun infer_formulas_types ctxt =
map_index (uncurry (fn j => set_var_index j #> Type.constraint HOLogic.boolT))
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
#> map (set_var_index 0)
@@ -607,7 +606,7 @@
nasty_atp_proof pool
#> map_term_names_in_atp_proof repair_name
#> map_filter (termify_line ctxt format type_enc lifted sym_tab)
- #> map_proof_terms (infer_formula_types ctxt #> map HOLogic.mk_Trueprop)
+ #> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop)
#> local_prover = waldmeisterN ? repair_waldmeister_endgame
fun take_distinct_vars seen ((t as Var _) :: ts) =
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Tue Jul 29 23:39:35 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Jul 30 00:50:41 2014 +0200
@@ -167,8 +167,9 @@
val subseqss = map (subsequents seqs) zones
val seqs = fold (subtract direct_sequent_eq) subseqss seqs
val cases = map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs)) c subseqss
+ val cases' = filter_out (null o snd) cases
in
- s_cases cases @ redirect (succedent_of_cases cases) proved seqs
+ s_cases cases' @ redirect (succedent_of_cases cases) proved seqs
end
in
redirect [] axioms seqs
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML Tue Jul 29 23:39:35 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Wed Jul 30 00:50:41 2014 +0200
@@ -181,7 +181,7 @@
val thy = Proof_Context.theory_of ctxt
val t = u
|> atp_to_trm
- |> singleton (infer_formula_types ctxt)
+ |> singleton (infer_formulas_types ctxt)
|> HOLogic.mk_Trueprop
in
(name, role, t, rule, deps)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jul 29 23:39:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 00:50:41 2014 +0200
@@ -108,7 +108,7 @@
val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
val datatype_methods = [Simp_Method, Simp_Size_Method]
val systematic_methods0 = basic_systematic_methods @ basic_arith_methods @ simp_based_methods @
- [Metis_Method (SOME no_typesN, NONE)]
+ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
val rewrite_methods = simp_based_methods @ basic_systematic_methods @ basic_arith_methods
val skolem_methods = basic_systematic_methods
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Tue Jul 29 23:39:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Jul 30 00:50:41 2014 +0200
@@ -65,8 +65,8 @@
update_proof proof (update_subproofs subproofs updates)
and update_proof proof (proofs, []) = (proof :: proofs, [])
| update_proof (Proof (fix, assms, steps)) (proofs, updates) =
- let val (steps, updates) = update_steps steps updates in
- (Proof (fix, assms, steps) :: proofs, updates)
+ let val (steps', updates') = update_steps steps updates in
+ (Proof (fix, assms, steps') :: proofs, updates')
end
in
fst (update_steps steps (rev updates))