# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID ac02112a208eb281ee18a2efbe1ed0bba24e36f7
# Parent  6c8170f8849e38b4465e057f91ffbc6f9c9c2d3b
remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"

diff -r 6c8170f8849e -r ac02112a208e doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 20:36:35 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Mon Jun 06 20:36:35 2011 +0200
@@ -751,9 +751,6 @@
 the external provers, Metis itself can be used for proof search.
 
 \item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
-
-\item[$\bullet$] \textbf{\textit{metisX}:} New experimental version of Metis,
-designed to subsume both \textit{metis} and \textit{metisFT}.
 \end{enum}
 
 In addition, the following remote provers are supported:
diff -r 6c8170f8849e -r ac02112a208e 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
@@ -17,7 +17,6 @@
   datatype reconstructor =
     Metis |
     MetisFT |
-    MetisX |
     SMT of string
 
   datatype play =
@@ -69,7 +68,6 @@
 datatype reconstructor =
   Metis |
   MetisFT |
-  MetisX |
   SMT of string
 
 datatype play =
@@ -255,7 +253,6 @@
 
 fun reconstructor_name Metis = "metis"
   | reconstructor_name MetisFT = "metisFT"
-  | reconstructor_name MetisX = "metisX"
   | reconstructor_name (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings
diff -r 6c8170f8849e -r ac02112a208e 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
@@ -12,9 +12,7 @@
   type type_sys = ATP_Translate.type_sys
 
   val metisN : string
-  val metisF_N : string
   val metisFT_N : string
-  val metisX_N : string
   val trace : bool Config.T
   val verbose : bool Config.T
   val new_skolemizer : bool Config.T
diff -r 6c8170f8849e -r ac02112a208e 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
@@ -129,8 +129,7 @@
    "Async_Manager". *)
 val das_tool = "Sledgehammer"
 
-val metis_prover_names =
-  [Metis_Tactics.metisN, Metis_Tactics.metisFT_N, Metis_Tactics.metisX_N]
+val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N]
 
 val is_metis_prover = member (op =) metis_prover_names
 val is_atp = member (op =) o supported_atps
@@ -419,8 +418,6 @@
 
 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)
   | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
 
 fun timed_reconstructor reconstructor debug timeout ths =
@@ -1016,7 +1013,6 @@
   let
     val reconstructor = if name = Metis_Tactics.metisN then Metis
                         else if name = Metis_Tactics.metisFT_N then MetisFT
-                        else if name = Metis_Tactics.metisX_N then MetisX
                         else raise Fail ("unknown Metis version: " ^ quote name)
     val (used_facts, used_ths) =
       facts |> map untranslated_fact |> ListPair.unzip