enable new Metis

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 06 20:36:36 2011 +0200
@@ -542,9 +542,9 @@
        else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
        else if full orelse !reconstructor = "metisFT" then
-         Metis_Tactics.old_metisFT_tac
+         Metis_Tactics.new_metisFT_tac
        else
-         Metis_Tactics.old_metis_tac) ctxt thms
+         Metis_Tactics.new_metis_tac []) ctxt thms
     fun apply_reconstructor thms =
       Mirabelle.can_apply timeout (do_reconstructor thms) st
 

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:36 2011 +0200
@@ -11,12 +11,13 @@
 sig
   val metisN : string
   val metisFT_N : string
+  val default_unsound_type_sys : string
+  val default_sound_type_sys : string
   val trace : bool Config.T
   val verbose : bool Config.T
   val new_skolemizer : bool Config.T
   val old_metis_tac : Proof.context -> thm list -> int -> tactic
   val old_metisF_tac : Proof.context -> thm list -> int -> tactic
-  val old_metisH_tac : Proof.context -> thm list -> int -> tactic
   val old_metisFT_tac : Proof.context -> thm list -> int -> tactic
   val new_metis_tac : string list -> Proof.context -> thm list -> int -> tactic
   val new_metisFT_tac : Proof.context -> thm list -> int -> tactic
@@ -30,23 +31,23 @@
 open Metis_Translate
 open Metis_Reconstruct
 
+val metisN = Binding.qualified_name_of @{binding metis}
+val metisFT_N = Binding.qualified_name_of @{binding metisFT}
 val full_typesN = "full_types"
-val default_unsound_type_sys = "poly_args"
-val default_sound_type_sys = "poly_preds_query"
 
-fun method_call_for_mode HO = (@{binding metis}, "")
+val default_unsound_type_sys = "poly_args"
+val default_sound_type_sys = "poly_preds_heavy_query"
+
+fun method_call_for_mode HO = (@{binding old_metis}, "")
   | method_call_for_mode FO = (@{binding metisF}, "")
-  | method_call_for_mode FT = (@{binding metisFT}, "")
+  | method_call_for_mode FT = (@{binding old_metisFT}, "")
   | method_call_for_mode (Type_Sys type_sys) =
     if type_sys = default_sound_type_sys then
-      (@{binding new_metisFT}, "")
+      (@{binding metisFT}, "")
     else
-      (@{binding new_metis},
+      (@{binding metis},
        if type_sys = default_unsound_type_sys then "" else type_sys)
 
-val metisN = Binding.qualified_name_of @{binding metis}
-val metisFT_N = Binding.qualified_name_of @{binding metisFT}
-
 val new_skolemizer =
   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
 
@@ -219,7 +220,6 @@
 
 val old_metis_modes = [HO, FT]
 val old_metisF_modes = [FO, FT]
-val old_metisH_modes = [HO]
 val old_metisFT_modes = [FT]
 val new_metis_default_modes =
   map Type_Sys [default_unsound_type_sys, default_sound_type_sys]
@@ -227,7 +227,6 @@
 
 val old_metis_tac = generic_metis_tac old_metis_modes
 val old_metisF_tac = generic_metis_tac old_metisF_modes
-val old_metisH_tac = generic_metis_tac old_metisH_modes
 val old_metisFT_tac = generic_metis_tac old_metisFT_modes
 fun new_metis_tac [] = generic_metis_tac new_metis_default_modes
   | new_metis_tac type_syss = generic_metis_tac (map Type_Sys type_syss)

--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:36 2011 +0200
@@ -376,8 +376,10 @@
 (*
 val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
 *)
+      (* "rev" is for compatibility *)
       val axioms =
         atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
+                    |> rev
     in
       (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
     end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:36 2011 +0200
@@ -416,8 +416,9 @@
     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
 
-fun tac_for_reconstructor Metis = Metis_Tactics.old_metisH_tac
-  | tac_for_reconstructor MetisFT = Metis_Tactics.old_metisFT_tac
+fun tac_for_reconstructor Metis =
+    Metis_Tactics.new_metis_tac [Metis_Tactics.default_unsound_type_sys]
+  | tac_for_reconstructor MetisFT = Metis_Tactics.new_metisFT_tac
   | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
 
 fun timed_reconstructor reconstructor debug timeout ths =

--- a/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/ex/CASC_Setup.thy	Mon Jun 06 20:36:36 2011 +0200
@@ -52,7 +52,7 @@
        THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "metis"
-       (ALLGOALS (Metis_Tactics.new_metis_tac ctxt NONE []))
+       (ALLGOALS (Metis_Tactics.new_metis_tac [] ctxt []))
    ORELSE
    SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
    ORELSE