diff -r 839f599bc7ed -r 467d5b34e1f5 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -17,6 +17,7 @@
   datatype reconstructor =
     Metis |
     MetisFT |
+    MetisX |
     SMT of string
 
   datatype play =
@@ -68,6 +69,7 @@
 datatype reconstructor =
   Metis |
   MetisFT |
+  MetisX |
   SMT of string
 
 datatype play =
@@ -253,6 +255,7 @@
 
 fun reconstructor_name Metis = "metis"
   | reconstructor_name MetisFT = "metisFT"
+  | reconstructor_name MetisX = "metisX"
   | reconstructor_name (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings
@@ -1023,7 +1026,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 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),