# HG changeset patch
# User blanchet
# Date 1406674241 -7200
# Node ID a6cf197c1f1e18063d7e2ba0128bb8f2cfd4cf6c
# Parent  afef6616cbae35c3ff48a3c2ef91d7afe05065bf
also try 'metis' with 'full_types'

diff -r afef6616cbae -r a6cf197c1f1e src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- 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) =
diff -r afef6616cbae -r a6cf197c1f1e src/HOL/Tools/ATP/atp_proof_redirect.ML
--- 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
diff -r afef6616cbae -r a6cf197c1f1e src/HOL/Tools/ATP/atp_waldmeister.ML
--- 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)
diff -r afef6616cbae -r a6cf197c1f1e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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
 
diff -r afef6616cbae -r a6cf197c1f1e src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- 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))