# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 45f33d2906156459ee9535021bacb3e93a4a22c4
# Parent  7a2bc89ac48e41dacb09b5a095a75b176c3491d1
make "metisX"'s default more like old "metis"

diff -r 7a2bc89ac48e -r 45f33d290615 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -1040,7 +1040,7 @@
        else
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
-    val reconstructor = if full_types then MetisX else Metis
+    val reconstructor = if full_types then MetisFT else Metis
     fun do_facts (ls, ss) =
       reconstructor_command reconstructor 1 1
           (ls |> sort_distinct (prod_ord string_ord int_ord),
diff -r 7a2bc89ac48e -r 45f33d290615 src/HOL/Tools/Metis/metis_tactics.ML
--- 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:35 2011 +0200
@@ -20,8 +20,8 @@
   val new_skolemizer : bool Config.T
   val metis_tac : Proof.context -> thm list -> int -> tactic
   val metisF_tac : Proof.context -> thm list -> int -> tactic
+  val metisH_tac : Proof.context -> thm list -> int -> tactic
   val metisFT_tac : Proof.context -> thm list -> int -> tactic
-  val metisHO_tac : Proof.context -> thm list -> int -> tactic
   val metisX_tac : Proof.context -> type_sys option -> thm list -> int -> tactic
   val setup : theory -> theory
 end
@@ -206,16 +206,16 @@
       Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
   end
 
-val metis_modes = [HO, MX]
-val metisF_modes = [FO, MX]
+val metis_modes = [HO, FT]
+val metisF_modes = [FO, FT]
+val metisH_modes = [HO]
 val metisFT_modes = [FT]
-val metisHO_modes = [HO]
 val metisX_modes = [MX]
 
 val metis_tac = generic_metis_tac metis_modes NONE
 val metisF_tac = generic_metis_tac metisF_modes NONE
+val metisH_tac = generic_metis_tac metisH_modes NONE
 val metisFT_tac = generic_metis_tac metisFT_modes NONE
-val metisHO_tac = generic_metis_tac metisHO_modes NONE
 fun metisX_tac ctxt type_sys = generic_metis_tac metisX_modes type_sys ctxt
 
 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
diff -r 7a2bc89ac48e -r 45f33d290615 src/HOL/Tools/Metis/metis_translate.ML
--- 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:35 2011 +0200
@@ -346,7 +346,8 @@
     end
   | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
 
-val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
+(* FIXME: put in "Metis_Tactics" as string *)
+val default_type_sys = Preds (Polymorphic, Const_Arg_Types, Lightweight)
 
 (* Function to generate metis clauses, including comb and type clauses *)
 fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =
diff -r 7a2bc89ac48e -r 45f33d290615 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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:35 2011 +0200
@@ -417,7 +417,7 @@
     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.metisHO_tac
+fun tac_for_reconstructor Metis = Metis_Tactics.metisH_tac
   | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
   | tac_for_reconstructor MetisX =
     (fn ctxt => Metis_Tactics.metisX_tac ctxt NONE)
@@ -790,7 +790,7 @@
                         |> map snd
               in
                 play_one_line_proof debug preplay_timeout used_ths state subgoal
-                                    [Metis, MetisX]
+                                    [Metis, MetisFT]
               end,
            fn preplay =>
               let
@@ -984,7 +984,7 @@
                 else "smt_solver = " ^ maybe_quote name
             in
               case play_one_line_proof debug preplay_timeout used_ths state
-                                       subgoal [Metis, MetisX] of
+                                       subgoal [Metis, MetisFT] of
                 p as Played _ => p
               | _ => Trust_Playable (SMT (smt_settings ()), NONE)
             end,