src/HOL/Tools/ATP/atp_reconstruct.ML

   type type_sys = ATP_Translate.type_sys
 
   datatype reconstructor =
     Metis |
     MetisFT |
+    MetisX |
     SMT of string
 
   datatype play =
     Played of reconstructor * Time.time |
     Trust_Playable of reconstructor * Time.time option|

 open ATP_Translate
 
 datatype reconstructor =
   Metis |
   MetisFT |
+  MetisX |
   SMT of string
 
 datatype play =
   Played of reconstructor * Time.time |
   Trust_Playable of reconstructor * Time.time option |

 
 (** Soft-core proof reconstruction: Metis one-liner **)
 
 fun reconstructor_name Metis = "metis"
   | reconstructor_name MetisFT = "metisFT"
+  | reconstructor_name MetisX = "metisX"
   | reconstructor_name (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings
   | reconstructor_settings _ = ""
 

       (if member (op =) qs Then then
          if member (op =) qs Show then "thus" else "hence"
        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 MetisFT else Metis
+    val reconstructor = if full_types then MetisX else Metis
     fun do_facts (ls, ss) =
       reconstructor_command reconstructor 1 1
           (ls |> sort_distinct (prod_ord string_ord int_ord),
            ss |> sort_distinct string_ord)
     and do_step ind (Fix xs) =